diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md
index be29f99..d48f530 100644
--- a/DEVELOPMENT.md
+++ b/DEVELOPMENT.md
@@ -38,7 +38,6 @@ Anytime you want to restart your project with the latest changes, you can just r
 ├── idris-model.coffee
 ├── language-idris.coffee
 ├── utils
-│   ├── Logger.coffee
 │   ├── dom.coffee
 │   ├── editor.coffee
 │   ├── highlighter.coffee
diff --git a/lib/idris-controller.ts b/lib/idris-controller.ts
index 5988767..54770ce 100644
--- a/lib/idris-controller.ts
+++ b/lib/idris-controller.ts
@@ -1,16 +1,15 @@
+import { spawn, ChildProcessWithoutNullStreams } from 'child_process'
 import {
     MessagePanelView,
     PlainMessageView,
     LineMessageView,
 } from 'atom-message-panel'
+import { IdrisClient, InfoReply, FinalReply, Reply } from 'idris-ide-client'
 import { InformationView } from './views/information-view'
 import { HolesView } from './views/holes-view'
-import Logger from './utils/Logger'
-import { IdrisModel } from './idris-model'
-import * as Ipkg from './utils/ipkg'
+import { browseNamespaceView } from './views/browse-namespace'
 import * as Symbol from './utils/symbol'
 import { getWordUnderCursor, moveToNextEmptyLine } from './utils/editor'
-import * as highlighter from './utils/highlighter'
 import {
     TextEditor,
     RangeCompatible,
@@ -18,10 +17,30 @@ import {
     Pane,
     WorkspaceOpenOptions,
 } from 'atom'
+import {
+    findAndReadIpkgFile,
+    compilerOptionsToFlags,
+    CompilerOptions,
+    defaultCompilerOptions,
+    sameCompilerOptions,
+} from './utils/ipkg'
+import { highlight, highlightToString } from './utils/highlighter'
+
+const replyCallback = (handleWarning: (reply: InfoReply.Warning) => void) => (
+    reply: Reply,
+): void => {
+    switch (reply.type) {
+        case ':warning':
+            return handleWarning(reply)
+        default:
+    }
+}
 
 export class IdrisController {
     errorMarkers: Array<DisplayMarker> = []
-    model: IdrisModel = new IdrisModel()
+    compilerOptions: CompilerOptions = defaultCompilerOptions
+    idrisProc: ChildProcessWithoutNullStreams
+    client: IdrisClient
     messages: MessagePanelView = new MessagePanelView({
         title: 'Idris Messages',
     })
@@ -49,6 +68,24 @@ export class IdrisController {
         this.openREPL = this.openREPL.bind(this)
         this.apropos = this.apropos.bind(this)
         this.displayErrors = this.displayErrors.bind(this)
+
+        const tabLength = atom.config.get('editor.tabLength', {
+            scope: ['source.idris'],
+        })
+
+        this.idrisProc = spawn('idris', [
+            '--ide-mode',
+            '--indent-with=' + tabLength,
+            '--indent-clause=' + tabLength,
+        ])
+        this.client = new IdrisClient(
+            this.idrisProc.stdin,
+            this.idrisProc.stdout,
+            {
+                replyCallback: replyCallback(this.handleWarning.bind(this)),
+            },
+        )
+        this.startCompiler()
     }
 
     getCommands() {
@@ -88,16 +125,18 @@ export class IdrisController {
     }
 
     // prefix code lines with "> "  if we are in the literate grammar
-    prefixLiterateClause(clause: Array<string>): Array<string> {
-        const birdPattern = new RegExp(`^\
->\
-(\\s)+\
-`)
-
+    prefixLiterateClause(clause: string): string {
         if (this.isLiterateGrammar()) {
-            return Array.from(clause).map((line: string) =>
-                line.match(birdPattern) ? line : '> ' + line,
-            )
+            const birdPattern = new RegExp(`^\
+            >\
+            (\\s)+\
+            `)
+            return clause
+                .split('\n')
+                .map((line: string) =>
+                    line.match(birdPattern) ? line : '> ' + line,
+                )
+                .join('\n')
         } else {
             return clause
         }
@@ -129,10 +168,7 @@ export class IdrisController {
     }
 
     destroy(): void {
-        if (this.model) {
-            Logger.logText('Idris: Shutting down!')
-            this.model.stop()
-        }
+        this.stopCompiler()
     }
 
     // clear the message panel and optionally display a new title
@@ -166,13 +202,6 @@ export class IdrisController {
         )
     }
 
-    initialize(compilerOptions: Ipkg.CompilerOptions): void {
-        this.destroyMarkers()
-        this.messages.attach()
-        this.messages.hide()
-        this.model.setCompilerOptions(compilerOptions)
-    }
-
     /**
      * Get the currently active text editor.
      */
@@ -184,17 +213,47 @@ export class IdrisController {
         return atom.workspace.getActivePane()
     }
 
-    stopCompiler(): boolean | undefined {
-        return this.model != null ? this.model.stop() : undefined
+    stopCompiler(): void {
+        if (this.idrisProc) {
+            this.idrisProc.kill()
+        }
+    }
+
+    async startCompiler(): Promise<IdrisClient> {
+        try {
+            const compilerOptions = await findAndReadIpkgFile(atom.project)
+            if (
+                compilerOptions &&
+                !sameCompilerOptions(this.compilerOptions, compilerOptions)
+            ) {
+                const tabLength = atom.config.get('editor.tabLength', {
+                    scope: ['source.idris'],
+                })
+
+                const flags = compilerOptionsToFlags(compilerOptions, tabLength)
+                this.stopCompiler()
+                this.compilerOptions = compilerOptions
+                this.idrisProc = spawn('idris', flags)
+                this.client = new IdrisClient(
+                    this.idrisProc.stdin,
+                    this.idrisProc.stdout,
+                    {
+                        replyCallback: replyCallback(
+                            this.handleWarning.bind(this),
+                        ),
+                    },
+                )
+            }
+            return this.client
+        } catch {
+            return this.client
+        }
     }
 
     runCommand(command: (args: any) => void) {
         return (args: any) => {
-            const compilerOptions = Ipkg.compilerOptions(atom.project)
-            return compilerOptions.subscribe((options: any) => {
-                Logger.logObject('Compiler Options:', options)
-                this.initialize(options)
-                return command(args)
+            this.startCompiler().then(() => {
+                command(args)
             })
         }
     }
@@ -213,18 +272,16 @@ export class IdrisController {
             getSuggestions: ({ prefix, activatedManually }: any) => {
                 const trimmedPrefix = prefix.trim()
                 if (trimmedPrefix.length > 2 || activatedManually) {
-                    return Ipkg.compilerOptions(atom.project)
-                        .flatMap((options: any) => {
-                            this.initialize(options)
-                            return this.model.replCompletions(trimmedPrefix)
+                    return this.startCompiler()
+                        .then(() => {
+                            return this.client.replCompletions(trimmedPrefix)
                         })
-                        .toPromise()
-                        .then(({ msg }: any) =>
-                            Array.from(msg[0][0]).map((sug) => ({
+                        .then((reply: FinalReply.ReplCompletions) => {
+                            return reply.completions.map((sug) => ({
                                 type: 'function',
                                 text: sug,
-                            })),
-                        )
+                            }))
+                        })
                 } else {
                     return null
                 }
@@ -262,18 +319,18 @@ export class IdrisController {
             return this.saveFile(editor).then((uri) => {
                 this.clearMessagePanel('Idris: Typechecking...')
 
-                const successHandler = () => {
-                    return this.clearMessagePanel(
-                        'Idris: File loaded successfully',
-                    )
+                const successHandler = (loadFile: FinalReply.LoadFile) => {
+                    if (loadFile.ok) {
+                        this.clearMessagePanel(
+                            'Idris: File loaded successfully',
+                        )
+                    }
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -287,28 +344,27 @@ export class IdrisController {
                     'Idris: Searching docs for <tt>' + word + '</tt> ...',
                 )
 
-                const successHandler = ({ msg }: any) => {
-                    const [type, highlightingInfo] = Array.from(msg)
-                    this.clearMessagePanel(
-                        'Idris: Docs for <tt>' + word + '</tt>',
-                    )
-
-                    const informationView = new InformationView()
-                    informationView.initialize({
-                        obligation: type,
-                        highlightingInfo,
-                    })
-                    return this.messages.add(informationView)
+                const successHandler = (docsFor: FinalReply.DocsFor) => {
+                    if (docsFor.ok) {
+                        this.clearMessagePanel(
+                            'Idris: Docs for <tt>' + word + '</tt>',
+                        )
+                        const informationView = new InformationView()
+                        informationView.initialize(
+                            docsFor.docs,
+                            docsFor.metadata,
+                        )
+                        this.messages.add(informationView)
+                    } else {
+                        this.rawMessage(docsFor.err)
+                    }
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.docsFor(word))
-                    .catch(() => this.model.docsFor(word))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.docsFor(word, ':full'))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -321,25 +377,26 @@ export class IdrisController {
                 this.clearMessagePanel(
                     'Idris: Searching type of <tt>' + word + '</tt> ...',
                 )
-                const successHandler = ({ msg }: any): void => {
-                    const [type, highlightingInfo] = msg
-                    this.clearMessagePanel(
-                        'Idris: Type of <tt>' + word + '</tt>',
-                    )
-                    const informationView = new InformationView()
-                    informationView.initialize({
-                        obligation: type,
-                        highlightingInfo,
-                    })
-                    this.messages.add(informationView)
+                const successHandler = (typeOf: FinalReply.TypeOf) => {
+                    if (typeOf.ok) {
+                        this.clearMessagePanel(
+                            'Idris: Type of <tt>' + word + '</tt>',
+                        )
+                        const informationView = new InformationView()
+                        informationView.initialize(
+                            typeOf.typeOf,
+                            typeOf.metadata,
+                        )
+                        this.messages.add(informationView)
+                    } else {
+                        this.rawMessage(typeOf.err)
+                    }
                 }
-                return this.model
-                    .load(uri)
-                    .filter((response: any) => {
-                        return response.responseType === 'return'
-                    })
-                    .flatMap(() => this.model.getType(word))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.typeOf(word))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -354,29 +411,26 @@ export class IdrisController {
 
                 this.clearMessagePanel('Idris: Do case split ...')
 
-                const successHandler = ({ msg }: any) => {
-                    const [split] = msg
-                    if (split === '') {
-                        // split returned nothing - cannot split
-                        return this.clearMessagePanel(
-                            'Idris: Cannot split ' + word,
-                        )
-                    } else {
+                const successHandler = (caseSplit: FinalReply.CaseSplit) => {
+                    if (caseSplit.ok) {
                         this.hideAndClearMessagePanel()
                         const lineRange = cursor.getCurrentLineBufferRange({
                             includeNewline: true,
                         })
-                        return editor.setTextInBufferRange(lineRange, split)
+                        return editor.setTextInBufferRange(
+                            lineRange,
+                            caseSplit.caseClause,
+                        )
+                    } else {
+                        this.clearMessagePanel('Idris: Cannot split ' + word)
                     }
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.caseSplit(line + 1, word))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.caseSplit(word, line + 1))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -389,14 +443,14 @@ export class IdrisController {
         if (editor) {
             return this.saveFile(editor).then((uri) => {
                 const line = editor.getLastCursor().getBufferRow()
-                // by adding a clause we make sure that the word is
-                // not treated as a symbol
                 const word = getWordUnderCursor(editor)
 
                 this.clearMessagePanel('Idris: Add clause ...')
 
-                const successHandler = ({ msg }: any) => {
-                    const [clause] = this.prefixLiterateClause(msg)
+                const successHandler = (addClause: FinalReply.AddClause) => {
+                    const clause = this.prefixLiterateClause(
+                        addClause.initialClause,
+                    )
 
                     this.hideAndClearMessagePanel()
 
@@ -414,13 +468,11 @@ export class IdrisController {
                     })
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.addClause(line + 1, word))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.addClause(word, line + 1))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -435,18 +487,15 @@ export class IdrisController {
                 const line = editor.getLastCursor().getBufferRow()
                 const word = getWordUnderCursor(editor)
                 this.clearMessagePanel('Idris: Add proof clause ...')
-
-                const successHandler = ({ msg }: any) => {
-                    const [clause] = this.prefixLiterateClause(msg)
-
+                const successHandler = (reply: FinalReply.AddClause) => {
+                    const clause = this.prefixLiterateClause(
+                        reply.initialClause,
+                    )
                     this.hideAndClearMessagePanel()
-
                     editor.transact(() => {
                         moveToNextEmptyLine(editor)
-
                         // Insert the new clause
                         editor.insertText(clause)
-
                         // And move the cursor to the beginning of
                         // the new line and add an empty line below it
                         editor.insertNewlineBelow()
@@ -454,14 +503,11 @@ export class IdrisController {
                         editor.moveToBeginningOfLine()
                     })
                 }
-
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.addProofClause(line + 1, word))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.addClause(word, line + 1))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -476,8 +522,8 @@ export class IdrisController {
 
                 this.clearMessagePanel('Idris: Make with view ...')
 
-                const successHandler = ({ msg }: any) => {
-                    const [clause] = Array.from(this.prefixLiterateClause(msg))
+                const successHandler = (reply: FinalReply.MakeWith) => {
+                    const clause = this.prefixLiterateClause(reply.withClause)
 
                     this.hideAndClearMessagePanel()
 
@@ -493,14 +539,11 @@ export class IdrisController {
                 }
 
                 if (word != null ? word.length : undefined) {
-                    return this.model
-                        .load(uri)
-                        .filter(
-                            ({ responseType }: any) =>
-                                responseType === 'return',
-                        )
-                        .flatMap(() => this.model.makeWith(line + 1, word))
-                        .subscribe(successHandler, this.displayErrors)
+                    return this.client
+                        .loadFile(uri)
+                        .then(() => this.client.makeWith(word, line + 1))
+                        .then(successHandler)
+                        .catch(this.displayErrors)
                 } else {
                     return this.clearMessagePanel(
                         'Idris: Illegal position to make a with view',
@@ -519,16 +562,19 @@ export class IdrisController {
                 const word = getWordUnderCursor(editor)
                 this.clearMessagePanel('Idris: Make lemma ...')
 
-                const successHandler = ({ msg }: any) => {
-                    // param1 contains the code which replaces the hole
-                    // param2 contains the code for the lemma function
-                    let [lemty, param1, param2] = msg
-                    param2 = this.prefixLiterateClause(param2)
+                const successHandler = (reply: FinalReply.MakeLemma) => {
+                    if ('err' in reply) {
+                        this.clearMessagePanel(
+                            'Idris: Cannot make lemma at ' + word,
+                        )
+                    } else {
+                        // metavariable contains the code which replaces the hole
+                        // declaration contains the code for the lemma function
+                        const { declaration, metavariable } = reply
 
-                    this.hideAndClearMessagePanel()
+                        this.hideAndClearMessagePanel()
 
-                    return editor.transact(function () {
-                        if (lemty === ':metavariable-lemma') {
+                        return editor.transact(function () {
                             // Move the cursor to the beginning of the word
                             editor.moveToBeginningOfWord()
                             // Because the ? in the Holes isn't part of
@@ -538,13 +584,11 @@ export class IdrisController {
                             editor.selectToEndOfWord()
                             editor.selectToEndOfWord()
                             // And then replace the replacement with the lemma call..
-                            editor.insertText(param1[1])
-
+                            editor.insertText(metavariable)
                             // Now move to the previous blank line and insert the type
                             // of the lemma
                             editor.moveToBeginningOfLine()
                             line = editor.getLastCursor().getBufferRow()
-
                             // I tried to make this a function but failed to find out how
                             // to call it and gave up...
                             while (line > 0) {
@@ -557,21 +601,18 @@ export class IdrisController {
                                 editor.moveUp()
                                 line--
                             }
-
                             editor.insertNewlineBelow()
-                            editor.insertText(param2[1])
+                            editor.insertText(declaration)
                             return editor.insertNewlineBelow()
-                        }
-                    })
+                        })
+                    }
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.makeLemma(line + 1, word))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.makeLemma(word, line + 1))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -585,8 +626,10 @@ export class IdrisController {
                 const word = getWordUnderCursor(editor)
                 this.clearMessagePanel('Idris: Make case ...')
 
-                const successHandler = ({ msg }: any) => {
-                    const [clause] = Array.from(this.prefixLiterateClause(msg))
+                const successHandler = (reply: FinalReply.MakeCase) => {
+                    const [clause] = Array.from(
+                        this.prefixLiterateClause(reply.caseClause),
+                    )
 
                     this.hideAndClearMessagePanel()
 
@@ -602,13 +645,11 @@ export class IdrisController {
                     })
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.makeCase(line + 1, word))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.makeCase(word, line + 1))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -620,21 +661,21 @@ export class IdrisController {
             return this.saveFile(editor).then((uri) => {
                 this.clearMessagePanel('Idris: Searching holes ...')
 
-                const successHandler = ({ msg }: any) => {
-                    const [holes] = msg
+                const successHandler = (
+                    metavariables: FinalReply.Metavariables,
+                ) => {
+                    debugger
                     this.clearMessagePanel('Idris: Holes')
                     const holesView = new HolesView()
-                    holesView.initialize(holes)
+                    holesView.initialize(metavariables)
                     this.messages.add(holesView)
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.holes(80))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.metavariables(80))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -650,8 +691,8 @@ export class IdrisController {
                 const word = getWordUnderCursor(editor)
                 this.clearMessagePanel('Idris: Searching proof ...')
 
-                const successHandler = ({ msg }: any) => {
-                    const [res] = msg
+                const successHandler = (reply: FinalReply.ProofSearch) => {
+                    const res = reply.solution
 
                     this.hideAndClearMessagePanel()
                     if (res.startsWith('?')) {
@@ -675,13 +716,11 @@ export class IdrisController {
                     }
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.proofSearch(line + 1, word))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.proofSearch(word, line + 1, []))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -690,48 +729,28 @@ export class IdrisController {
         const editor = this.getEditor()
         if (editor) {
             return this.saveFile(editor).then((uri) => {
-                let nameSpace = editor.getSelectedText()
+                let nameSpace = editor.getSelectedText().trim()
 
                 this.clearMessagePanel(
                     'Idris: Browsing namespace <tt>' + nameSpace + '</tt>',
                 )
 
-                const successHandler = ({ msg }: any) => {
-                    // the information is in a two dimensional array
-                    // one array contains the namespaces contained in the namespace
-                    // and the seconds all the methods
-                    const namesSpaceInformation = msg[0][0]
-                    for (nameSpace of namesSpaceInformation) {
-                        this.rawMessage(nameSpace)
+                const successHandler = (reply: FinalReply.BrowseNamespace) => {
+                    if (reply.ok) {
+                        const view = browseNamespaceView(reply)
+                        this.messages.add(view)
+                    } else {
+                        this.clearMessagePanel(
+                            'Idris: Browse Namespace was not successful.',
+                        )
                     }
-
-                    const methodInformation = msg[0][1]
-                    return (() => {
-                        const result = []
-                        for (let [
-                            line,
-                            highlightInformation,
-                        ] of methodInformation) {
-                            const highlighting = highlighter.highlight(
-                                line,
-                                highlightInformation,
-                            )
-                            const info = highlighter.highlightToString(
-                                highlighting,
-                            )
-                            result.push(this.rawMessage(info))
-                        }
-                        return result
-                    })()
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.browseNamespace(nameSpace))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.browseNamespace(nameSpace))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -748,27 +767,31 @@ export class IdrisController {
                     'Idris: Searching definition of <tt>' + word + '</tt> ...',
                 )
 
-                const successHandler = ({ msg }: any) => {
-                    const [type, highlightingInfo] = Array.from(msg)
-                    this.clearMessagePanel(
-                        'Idris: Definition of <tt>' + word + '</tt>',
-                    )
-                    const informationView = new InformationView()
-                    informationView.initialize({
-                        obligation: type,
-                        highlightingInfo,
-                    })
-                    return this.messages.add(informationView)
+                const successHandler = (reply: FinalReply.PrintDefinition) => {
+                    if (reply.ok) {
+                        this.clearMessagePanel(
+                            'Idris: Definition of <tt>' + word + '</tt>',
+                        )
+                        const informationView = new InformationView()
+                        informationView.initialize(
+                            reply.definition,
+                            reply.metadata,
+                        )
+                        this.messages.add(informationView)
+                    } else {
+                        this.clearMessagePanel(
+                            'Idris: Error getting definition of <tt>' +
+                                word +
+                                '</tt>',
+                        )
+                    }
                 }
 
-                return this.model
-                    .load(uri)
-                    .filter(
-                        ({ responseType }: any) => responseType === 'return',
-                    )
-                    .flatMap(() => this.model.printDefinition(word))
-                    .catch(() => this.model.printDefinition(word))
-                    .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(() => this.client.printDefinition(word))
+                    .then(successHandler)
+                    .catch(this.displayErrors)
             })
         }
     }
@@ -779,24 +802,23 @@ export class IdrisController {
     openREPL() {
         const editor = this.getEditor()
         if (editor) {
-            const uri = editor.getPath() as any
-            this.clearMessagePanel('Idris: opening REPL ...')
-
-            const successHandler = () => {
-                this.hideAndClearMessagePanel()
+            return this.saveFile(editor).then((uri) => {
+                this.clearMessagePanel('Idris: opening REPL ...')
 
-                const options: WorkspaceOpenOptions = {
-                    split: 'right',
-                    searchAllPanes: true,
+                const successHandler = () => {
+                    this.hideAndClearMessagePanel()
+                    const options: WorkspaceOpenOptions = {
+                        split: 'right',
+                        searchAllPanes: true,
+                    }
+                    atom.workspace.open('idris://repl', options)
                 }
 
-                atom.workspace.open('idris://repl', options)
-            }
-
-            return this.model
-                .load(uri)
-                .filter(({ responseType }: any) => responseType === 'return')
-                .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(successHandler)
+                    .catch(this.displayErrors)
+            })
         }
     }
 
@@ -806,90 +828,67 @@ export class IdrisController {
     apropos() {
         const editor = this.getEditor()
         if (editor) {
-            const uri = editor.getPath() as any
-            this.clearMessagePanel('Idris: opening apropos view ...')
-
-            const successHandler = () => {
-                this.hideAndClearMessagePanel()
-
-                const options: WorkspaceOpenOptions = {
-                    split: 'right',
-                    searchAllPanes: true,
+            return this.saveFile(editor).then((uri) => {
+                this.clearMessagePanel('Idris: opening apropos view ...')
+                const successHandler = () => {
+                    this.hideAndClearMessagePanel()
+                    const options: WorkspaceOpenOptions = {
+                        split: 'right',
+                        searchAllPanes: true,
+                    }
+                    return atom.workspace.open('idris://apropos', options)
                 }
-
-                return atom.workspace.open('idris://apropos', options)
-            }
-
-            return this.model
-                .load(uri)
-                .filter(({ responseType }: any) => responseType === 'return')
-                .subscribe(successHandler, this.displayErrors)
+                return this.client
+                    .loadFile(uri)
+                    .then(successHandler)
+                    .catch(this.displayErrors)
+            })
         }
     }
 
+    displayErrors(_e: any) {
+        this.clearMessagePanel(
+            '<i class="icon-bug"></i> There was a fatal error',
+        )
+    }
+
     // generic function to display errors in the status bar
-    displayErrors(err: any) {
+    handleWarning(reply: InfoReply.Warning) {
+        const { err } = reply
+        const { warning, metadata, start, end, filename } = err
+
         this.clearMessagePanel('<i class="icon-bug"></i> Idris Errors')
 
-        // display the general error message
-        if (err.message != null) {
-            this.rawMessage(err.message)
-        }
+        const highlighting = highlight(warning, metadata)
+        const info = highlightToString(highlighting)
 
-        return (() => {
-            const result = []
-            for (let warning of err.warnings) {
-                const type = warning[3]
-                const highlightingInfo = warning[4]
-                const highlighting = highlighter.highlight(
-                    type,
-                    highlightingInfo,
-                )
-                const info = highlighter.highlightToString(highlighting)
-
-                const line = warning[1][0]
-                const character = warning[1][1]
-                const uri = warning[0].replace('./', err.cwd + '/')
-
-                // this provides information about the line and column of the error
-                this.messages.add(
-                    new LineMessageView({
-                        line,
-                        character,
-                        file: uri,
-                    }),
-                )
+        // this provides information about the line and column of the error
+        this.messages.add(
+            new LineMessageView({
+                message: info,
+                character: start.column,
+                line: start.line,
+                file: filename,
+            }),
+        )
 
-                // this provides a highlighted version of the error message
-                // returned by idris
-                this.rawMessage(info)
-
-                const editor = atom.workspace.getActiveTextEditor()
-                if (editor && line > 0 && uri === editor.getPath()) {
-                    const startPoint = warning[1]
-                    startPoint[0] = startPoint[0] - 1
-                    const endPoint = warning[2]
-                    endPoint[0] = endPoint[0] - 1
-                    const gutterMarker = this.createMarker(
-                        editor,
-                        [startPoint, endPoint],
-                        'line-number',
-                    )
-                    const lineMarker = this.createMarker(
-                        editor,
-                        [
-                            [line - 1, character - 1],
-                            [line, 0],
-                        ],
-                        'line',
-                    )
-                    this.errorMarkers.push(gutterMarker)
-                    result.push(this.errorMarkers.push(lineMarker))
-                } else {
-                    result.push(undefined)
-                }
-            }
-            return result
-        })()
+        const editor = atom.workspace.getActiveTextEditor()
+        if (editor && start.line > 0 && filename === editor.getPath()) {
+            const startPoint = { row: start.line - 1, column: start.column }
+            const endPoint = { row: end.line - 1, column: end.column }
+
+            const gutterMarker = this.createMarker(
+                editor,
+                [startPoint, endPoint],
+                'line-number',
+            )
+            const lineMarker = this.createMarker(
+                editor,
+                [startPoint, startPoint],
+                'line',
+            )
+            this.errorMarkers.push(gutterMarker)
+            this.errorMarkers.push(lineMarker)
+        }
     }
 }
diff --git a/lib/idris-ide-mode.ts b/lib/idris-ide-mode.ts
deleted file mode 100644
index 4a42723..0000000
--- a/lib/idris-ide-mode.ts
+++ /dev/null
@@ -1,133 +0,0 @@
-import Logger from './utils/Logger'
-import * as sexpFormatter from './protocol/sexp-formatter'
-import * as parse from './utils/parse'
-import { EventEmitter } from 'events'
-import { spawn, ChildProcessWithoutNullStreams } from 'child_process'
-import { SExp } from './protocol/ide-protocol'
-import { CompilerOptions } from './utils/ipkg'
-
-export class IdrisIdeMode extends EventEmitter {
-    process: ChildProcessWithoutNullStreams | null = null
-    buffer = ''
-    idrisBuffers = 0
-
-    start(compilerOptions: CompilerOptions) {
-        if (this.process == null || this.process.killed) {
-            const pathToIdris: string = atom.config.get(
-                'language-idris.pathToIdris',
-            )
-            const pkgs: Array<string> = (() => {
-                if (compilerOptions.pkgs && compilerOptions.pkgs.length) {
-                    const p = compilerOptions.pkgs.map((p) => ['-p', p]) as any
-                    return [].concat.apply([], p)
-                } else {
-                    return []
-                }
-            })()
-
-            let ipkgOptions = compilerOptions.options
-                ? compilerOptions.options.split(' ')
-                : []
-
-            const tabLength = atom.config.get('editor.tabLength', {
-                scope: ['source.idris'],
-            })
-            const configParams = [
-                '--ide-mode',
-                '--indent-with=' + tabLength,
-                '--indent-clause=' + tabLength,
-            ]
-
-            const parameters = configParams.concat(pkgs, ipkgOptions)
-
-            const options = compilerOptions.src
-                ? { cwd: compilerOptions.src }
-                : {}
-            this.process = spawn(pathToIdris, parameters, options)
-            this.process.on('error', this.error)
-            this.process.on('exit', this.exited)
-            this.process.on('close', this.exited)
-            this.process.on('disconnect', this.exited)
-
-            return this.process.stdout
-                .setEncoding('utf8')
-                .on('data', this.stdout.bind(this))
-        }
-    }
-
-    send(cmd: SExp): void {
-        if (this.process) {
-            Logger.logOutgoingCommand(cmd)
-            const serializedCommand = sexpFormatter.serialize(cmd)
-            console.log('serializedCommand', serializedCommand)
-            this.process.stdin.write(serializedCommand)
-        } else {
-            Logger.logText('Could not send command to the idris compiler')
-            Logger.logOutgoingCommand(cmd)
-        }
-    }
-
-    stop() {
-        return this.process != null ? this.process.kill() : undefined
-    }
-
-    error(error: any) {
-        const e =
-            error.code === 'ENOENT'
-                ? {
-                      short: "Couldn't find idris executable",
-                      long: `Couldn't find idris executable at \"${error.path}\"`,
-                  }
-                : {
-                      short: error.code,
-                      long: error.message,
-                  }
-
-        return atom.notifications.addError(e.short, { detail: e.long })
-    }
-
-    exited(code: number, signal: NodeJS.Signals) {
-        let long, short
-        if (signal === 'SIGTERM') {
-            short = 'The idris compiler was closed'
-            long = 'You stopped the compiler'
-            return atom.notifications.addInfo(short, { detail: long })
-        } else {
-            short = 'The idris compiler was closed or crashed'
-            long = signal
-                ? `It was closed with the signal: ${signal}`
-                : `It (probably) crashed with the error code: ${code}`
-            return atom.notifications.addError(short, { detail: long })
-        }
-    }
-
-    running(): boolean {
-        return !!this.process && !this.process.killed
-    }
-
-    stdout(data: string): Array<boolean> {
-        this.buffer += data
-        const result = []
-        while (this.buffer.length > 6) {
-            this.buffer = this.buffer.trimLeft().replace(/\r\n/g, '\n')
-            // We have 6 chars, which is the length of the command
-            const len = parseInt(this.buffer.substr(0, 6), 16)
-            if (this.buffer.length >= 6 + len) {
-                // We also have the length of the command in the buffer, so
-                // let's read in the command
-                const cmd = this.buffer.substr(6, len).trim()
-                Logger.logIncomingCommand(cmd)
-                // Remove the length + command from the buffer
-                this.buffer = this.buffer.substr(6 + len)
-                // And then we can try to parse to command..
-                const obj = parse.parseCommand(cmd.trim())
-                result.push(this.emit('message', obj))
-            } else {
-                // We didn't have the entire command, so let's break the
-                // while-loop and wait for the next data-event
-                break
-            }
-        }
-        return result
-    }
-}
diff --git a/lib/idris-model.ts b/lib/idris-model.ts
deleted file mode 100644
index 5bdd8a8..0000000
--- a/lib/idris-model.ts
+++ /dev/null
@@ -1,222 +0,0 @@
-import { IdrisIdeMode } from './idris-ide-mode'
-import * as Rx from 'rx-lite'
-import * as JS from './utils/js'
-import * as path from 'path'
-import { CompilerOptions } from './utils/ipkg'
-import { IDECommand, SExp } from './protocol/ide-protocol'
-import { ideCommandToSExp } from './protocol/to-sexp'
-import Logger from './utils/Logger'
-
-export class IdrisModel {
-    requestId = 0
-    ideModeRef: IdrisIdeMode | null = null
-    subjects: { [id: number]: Rx.Subject<any> } = {}
-    warnings: any = {}
-    compilerOptions: CompilerOptions = { pkgs: [] }
-    oldCompilerOptions: CompilerOptions = { pkgs: [] }
-
-    constructor() {
-        this.handleCommand = this.handleCommand.bind(this)
-    }
-
-    ideMode(compilerOptions: any) {
-        if (
-            this.ideModeRef &&
-            (!JS.objectEqual(this.oldCompilerOptions, compilerOptions) ||
-                !this.ideModeRef.running())
-        ) {
-            this.ideModeRef.process?.removeAllListeners()
-            this.ideModeRef.stop()
-            this.ideModeRef = null
-        }
-        if (!this.ideModeRef) {
-            this.ideModeRef = new IdrisIdeMode()
-            this.ideModeRef.on('message', this.handleCommand)
-            this.ideModeRef.start(compilerOptions)
-            this.oldCompilerOptions = compilerOptions
-        }
-        return this.ideModeRef
-    }
-
-    stop() {
-        return this.ideModeRef != null ? this.ideModeRef.stop() : undefined
-    }
-
-    setCompilerOptions(options: CompilerOptions): void {
-        this.compilerOptions = options
-    }
-
-    handleCommand(cmd: any) {
-        if (cmd.length > 0) {
-            const op = cmd[0],
-                adjustedLength = Math.max(cmd.length, 2),
-                params = cmd.slice(1, adjustedLength - 1),
-                id = cmd[adjustedLength - 1]
-            if (this.subjects[id] != null) {
-                const subject = this.subjects[id]
-                switch (op) {
-                    case ':return':
-                        var ret = params[0]
-                        if (ret[0] === ':ok') {
-                            const okparams = ret[1]
-                            if (okparams[0] === ':metavariable-lemma') {
-                                subject.onNext({
-                                    responseType: 'return',
-                                    msg: okparams,
-                                })
-                            } else {
-                                subject.onNext({
-                                    responseType: 'return',
-                                    msg: ret.slice(1),
-                                })
-                            }
-                        } else {
-                            subject.onError({
-                                message: ret[1],
-                                warnings: this.warnings[id],
-                                highlightInformation: ret[2],
-                                cwd: this.compilerOptions.src,
-                            })
-                        }
-                        subject.onCompleted()
-                        return delete this.subjects[id]
-                    case ':write-string':
-                        var msg = params[0]
-                        atom.notifications.addInfo(msg)
-                        return subject.onNext({
-                            responseType: 'write-string',
-                            msg,
-                        })
-                    case ':warning':
-                        var warning = params[0]
-                        return this.warnings[id].push(warning)
-                    case ':run-program':
-                        var options = {
-                            detail:
-                                'The path for the compiled program. It was copied to your clipboard. Paste it into a terminal to execute.',
-                            dismissible: true,
-                            icon: 'comment',
-                            buttons: [{ text: 'Confirm' }],
-                        }
-                        atom.clipboard.write(params[0])
-                        return atom.notifications.addSuccess(params[0], options)
-                    case ':set-prompt':
-                    // Ignore
-                    default: {
-                        Logger.logObject('Unhandled Operator', op)
-                        Logger.logObject('Params', params)
-                        return
-                    }
-                }
-            }
-        }
-    }
-
-    getUID(): number {
-        return ++this.requestId
-    }
-
-    prepareCommand(cmd: IDECommand): Rx.Subject<unknown> {
-        const id = this.getUID()
-        const subject = new Rx.Subject()
-        this.subjects[id] = subject
-        this.warnings[id] = []
-        const command: SExp = {
-            type: 'list',
-            data: [ideCommandToSExp(cmd), { type: 'integer', data: id }],
-        }
-        this.ideMode(this.compilerOptions).send(command)
-        return subject
-    }
-
-    changeDirectory(dir: string) {
-        return this.interpret(`:cd ${dir}`)
-    }
-
-    load(uri: string) {
-        const dir = this.compilerOptions.src
-            ? this.compilerOptions.src
-            : path.dirname(uri)
-
-        const cd = (() => {
-            if (dir !== this.compilerOptions.src) {
-                this.compilerOptions.src = dir
-                return this.changeDirectory(dir).map(() => dir)
-            } else {
-                return Rx.Observable.of(dir)
-            }
-        })()
-
-        return cd.flatMap((_) => {
-            return this.prepareCommand({ type: 'load-file', fileName: uri })
-        })
-    }
-
-    docsFor(symbolName: string) {
-        return this.prepareCommand({
-            type: 'docs-for',
-            symbolName,
-            mode: 'full',
-        })
-    }
-
-    replCompletions(name: string) {
-        return this.prepareCommand({ type: 'repl-completions', name })
-    }
-
-    getType(code: string) {
-        return this.prepareCommand({ type: 'type-of', code })
-    }
-
-    caseSplit(line: number, symbolName: string) {
-        return this.prepareCommand({ type: 'case-split', line, symbolName })
-    }
-
-    makeWith(line: number, symbolName: string) {
-        return this.prepareCommand({ type: 'make-with', line, symbolName })
-    }
-
-    makeLemma(line: number, symbolName: string) {
-        return this.prepareCommand({ type: 'make-lemma', line, symbolName })
-    }
-
-    interpret(code: string) {
-        return this.prepareCommand({ type: 'interpret', code })
-    }
-
-    makeCase(line: number, symbolName: string) {
-        return this.prepareCommand({ type: 'make-case', line, symbolName })
-    }
-
-    addClause(line: number, symbolName: string) {
-        return this.prepareCommand({ type: 'add-clause', line, symbolName })
-    }
-
-    addProofClause(line: number, symbolName: string) {
-        return this.prepareCommand({
-            type: 'add-proof-clause',
-            line,
-            symbolName,
-        })
-    }
-
-    holes(width: number) {
-        return this.prepareCommand({ type: 'metavariables', width })
-    }
-
-    proofSearch(line: number, symbolName: string) {
-        return this.prepareCommand({ type: 'proof-search', line, symbolName })
-    }
-
-    printDefinition(symbolName: string) {
-        return this.prepareCommand({ type: 'print-definition', symbolName })
-    }
-
-    apropos(code: string) {
-        return this.prepareCommand({ type: 'apropos', code })
-    }
-
-    browseNamespace(namespace: string) {
-        return this.prepareCommand({ type: 'browse-namespace', namespace })
-    }
-}
diff --git a/lib/protocol/ide-protocol.ts b/lib/protocol/ide-protocol.ts
deleted file mode 100644
index 47b1fed..0000000
--- a/lib/protocol/ide-protocol.ts
+++ /dev/null
@@ -1,167 +0,0 @@
-export type SExpList = { type: 'list'; data: Array<SExp> }
-export type StringAtom = { type: 'string'; data: string }
-export type BoolAtom = { type: 'bool'; data: boolean }
-export type IntegerAtom = { type: 'integer'; data: number }
-export type SymbolAtom = { type: 'symbol'; data: string }
-export type SExp = SExpList | StringAtom | BoolAtom | IntegerAtom | SymbolAtom
-
-/**
- * Interpret `code` at the Idris REPL, returning a highlighted result.
- */
-export type InterpretCommand = { type: 'interpret'; code: string }
-
-/**
- * Load the named file.
- * If `lineNumber` is provided, the file is only loaded up to that line. Otherwise, the entire file is loaded.
- */
-export type LoadFileCommand = {
-    type: 'load-file'
-    fileName: string
-    lineNumber?: number
-}
-
-/**
- * Return the type of the name, written with Idris syntax in the `code`.
- * The reply may contain highlighting information.
- */
-export type TypeOfCommand = { type: 'type-of'; code: string }
-
-type DocsForMode = 'overview' | 'full'
-/** Look up the documentation for NAME, and return it as a highlighted string.
- * If `mode` is `"overview"`, only the first paragraph of documentation is provided for `symbolName`.
- * If `mode` is `"full"`, or omitted, the full documentation is returned for `symbolName`.
- */
-export type DocsForComand = {
-    type: 'docs-for'
-    symbolName: string
-    mode: DocsForMode
-}
-
-/**
- * Generate a case-split for the pattern variable `symbolName` on program line `line`.
- * The pattern-match cases to be substituted are returned as a string with no highlighting.
- */
-export type CaseSplitCommand = {
-    type: 'case-split'
-    line: number
-    symbolName: string
-}
-
-/**
- * Generate an initial pattern-match clause for the function declared as `symbolName` on program line `line`.
- * The initial clause is returned as a string with no highlighting.
- */
-export type AddClauseCommand = {
-    type: 'add-clause'
-    line: number
-    symbolName: string
-}
-
-/**
- * Add a clause driven by the <== syntax.
- */
-export type AddProofClauseCommand = {
-    type: 'add-proof-clause'
-    line: number
-    symbolName: string
-}
-
-/**
- * Create a with-rule pattern match template for the clause of function `symbolName` on line `line`.
- * The new code is returned with no highlighting.
- */
-export type MakeWithCommand = {
-    type: 'make-with'
-    line: number
-    symbolName: string
-}
-
-/**
- * Create a top level function with a type which solves the hole named `symbolName` on line `line`.
- */
-export type MakeLemmaCommand = {
-    type: 'make-lemma'
-    line: number
-    symbolName: string
-}
-
-/**
- * Create a case pattern match template for the clause of function `symbolName` on line `line`.
- * The new code is returned with no highlighting.
- */
-export type MakeCaseCommand = {
-    type: 'make-case'
-    line: number
-    symbolName: string
-}
-
-/**
- * List the currently-active holes, with their types pretty-printed with `width` columns.
- */
-export type MetavariablesComand = {
-    type: 'metavariables'
-    width: number
-}
-
-/**
- * Attempt to fill out the holes on `line` named `symbolName` by proof search.
- */
-export type ProofSearchCommand = {
-    type: 'proof-search'
-    line: number
-    symbolName: string
-}
-
-/**
- * Return the definition of `symbolName` as a highlighted string.
- */
-export type PrintDefinitionCommand = {
-    type: 'print-definition'
-    symbolName: string
-}
-
-/**
- * Return the contents of `namespace`, like :browse at the command-line REPL.
- */
-export type BrowseNamespaceCommand = {
-    type: 'browse-namespace'
-    namespace: string
-}
-
-/**
- * Search the documentation for mentions of `code`, and return any found as a list of highlighted strings.
- */
-export type AproposCommand = {
-    type: 'apropos'
-    code: string
-}
-
-/**
- * Search names, types and documentations which contain `name`.
- * Return the result of tab-completing NAME as a REPL command.
- */
-export type ReplCompletionsCommand = {
-    type: 'repl-completions'
-    name: string
-}
-
-/**
- * IDE commands we can send to Idris
- */
-export type IDECommand =
-    | InterpretCommand
-    | LoadFileCommand
-    | TypeOfCommand
-    | DocsForComand
-    | CaseSplitCommand
-    | AddClauseCommand
-    | AddProofClauseCommand
-    | MakeWithCommand
-    | MakeLemmaCommand
-    | MakeCaseCommand
-    | MetavariablesComand
-    | ProofSearchCommand
-    | PrintDefinitionCommand
-    | BrowseNamespaceCommand
-    | AproposCommand
-    | ReplCompletionsCommand
diff --git a/lib/protocol/sexp-formatter.ts b/lib/protocol/sexp-formatter.ts
deleted file mode 100644
index faaecd1..0000000
--- a/lib/protocol/sexp-formatter.ts
+++ /dev/null
@@ -1,43 +0,0 @@
-import { SExp } from './ide-protocol'
-
-/*
- * Takes an s-expression and formats it for sending.
- * It serializes it, adds a newline at the end and
- * prepends it with the length of the command.
- */
-export const serialize = function (sexp: SExp) {
-    const msg = formatSexp(sexp) + '\n'
-    return `${hexLength(msg)}${msg}`
-}
-
-/**
- * Returns a 0-padded 6-char long hexadecimal
- * for the length of the input `str`
- */
-export const hexLength = function (str: string) {
-    const hex = str.length.toString(16)
-    return Array(7 - hex.length).join('0') + hex
-}
-
-/**
- * Serializes an s-expression.
- */
-export const formatSexp = (sexp: SExp): string => {
-    switch (sexp.type) {
-        case 'list': {
-            return `(${sexp.data.map(formatSexp).join(' ')})`
-        }
-        case 'string': {
-            return `"${sexp.data.trim()}"`
-        }
-        case 'bool': {
-            return sexp.data ? ':True' : ':False'
-        }
-        case 'integer': {
-            return `${sexp.data}`
-        }
-        case 'symbol': {
-            return `:${sexp.data.trim()}`
-        }
-    }
-}
diff --git a/lib/protocol/to-sexp.ts b/lib/protocol/to-sexp.ts
deleted file mode 100644
index 1af8cf3..0000000
--- a/lib/protocol/to-sexp.ts
+++ /dev/null
@@ -1,249 +0,0 @@
-import {
-    InterpretCommand,
-    TypeOfCommand,
-    SExp,
-    IDECommand,
-    LoadFileCommand,
-    DocsForComand,
-    SymbolAtom,
-    StringAtom,
-    CaseSplitCommand,
-    AddClauseCommand,
-    AddProofClauseCommand,
-    MakeWithCommand,
-    MakeLemmaCommand,
-    MakeCaseCommand,
-    MetavariablesComand,
-    ProofSearchCommand,
-    PrintDefinitionCommand,
-    BrowseNamespaceCommand,
-    AproposCommand,
-    ReplCompletionsCommand,
-} from './ide-protocol'
-
-// See: https://github.com/edwinb/Idris2-boot/blob/master/src/Idris/IDEMode/Commands.idr
-
-const interpretCommandToSExp = (cmd: InterpretCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'interpret' },
-            { type: 'string', data: cmd.code },
-        ],
-    }
-}
-
-const loadFileCommandToSExp = (cmd: LoadFileCommand): SExp => {
-    const commandSymbol: SymbolAtom = { type: 'symbol', data: 'load-file' }
-    const fileName: StringAtom = { type: 'string', data: cmd.fileName }
-    return {
-        type: 'list',
-        data: cmd.lineNumber
-            ? [
-                  commandSymbol,
-                  fileName,
-                  { type: 'integer', data: cmd.lineNumber },
-              ]
-            : [commandSymbol, fileName],
-    }
-}
-
-const typeOfCommandToSExp = (cmd: TypeOfCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'interpret' },
-            { type: 'string', data: cmd.code },
-        ],
-    }
-}
-
-const docsForComandToSExp = (cmd: DocsForComand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'docs-for' },
-            { type: 'string', data: cmd.symbolName },
-            { type: 'symbol', data: cmd.mode },
-        ],
-    }
-}
-
-const caseSplitCommandToSExp = (cmd: CaseSplitCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'case-split' },
-            { type: 'integer', data: cmd.line },
-            { type: 'string', data: cmd.symbolName },
-        ],
-    }
-}
-
-const addClauseCommandToSExp = (cmd: AddClauseCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'add-clause' },
-            { type: 'integer', data: cmd.line },
-            { type: 'string', data: cmd.symbolName },
-        ],
-    }
-}
-
-const addProofClauseCommandToSExp = (cmd: AddProofClauseCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'add-proof-clause' },
-            { type: 'integer', data: cmd.line },
-            { type: 'string', data: cmd.symbolName },
-        ],
-    }
-}
-
-const makeWithCommandToSExp = (cmd: MakeWithCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'make-case' },
-            { type: 'integer', data: cmd.line },
-            { type: 'string', data: cmd.symbolName },
-        ],
-    }
-}
-const makeLemmaCommandToSExp = (cmd: MakeLemmaCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'make-lemma' },
-            { type: 'integer', data: cmd.line },
-            { type: 'string', data: cmd.symbolName },
-        ],
-    }
-}
-
-const makeCaseCommandToSExp = (cmd: MakeCaseCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'make-case' },
-            { type: 'integer', data: cmd.line },
-            { type: 'string', data: cmd.symbolName },
-        ],
-    }
-}
-
-const metavariablesCommandToSExp = (cmd: MetavariablesComand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'metavariables' },
-            { type: 'integer', data: cmd.width },
-        ],
-    }
-}
-
-const proofSearchCommandToSExp = (cmd: ProofSearchCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'proof-search' },
-            { type: 'integer', data: cmd.line },
-            { type: 'string', data: cmd.symbolName },
-        ],
-    }
-}
-
-const printDefinitionCommandToSExp = (cmd: PrintDefinitionCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'print-definition' },
-            { type: 'string', data: cmd.symbolName },
-        ],
-    }
-}
-
-const browseNamespaceCommandToSepx = (cmd: BrowseNamespaceCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'browse-namespace' },
-            { type: 'string', data: cmd.namespace },
-        ],
-    }
-}
-
-const aproposCommandToSExp = (cmd: AproposCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'apropos' },
-            { type: 'string', data: cmd.code },
-        ],
-    }
-}
-
-const replCompletionCommandToSExp = (cmd: ReplCompletionsCommand): SExp => {
-    return {
-        type: 'list',
-        data: [
-            { type: 'symbol', data: 'repl-completions' },
-            { type: 'string', data: cmd.name },
-        ],
-    }
-}
-
-export const ideCommandToSExp = (cmd: IDECommand): SExp => {
-    switch (cmd.type) {
-        case 'interpret': {
-            return interpretCommandToSExp(cmd)
-        }
-        case 'load-file': {
-            return loadFileCommandToSExp(cmd)
-        }
-        case 'type-of': {
-            return typeOfCommandToSExp(cmd)
-        }
-        case 'docs-for': {
-            return docsForComandToSExp(cmd)
-        }
-        case 'case-split': {
-            return caseSplitCommandToSExp(cmd)
-        }
-        case 'add-clause': {
-            return addClauseCommandToSExp(cmd)
-        }
-        case 'add-proof-clause': {
-            return addProofClauseCommandToSExp(cmd)
-        }
-        case 'make-with': {
-            return makeWithCommandToSExp(cmd)
-        }
-        case 'make-lemma': {
-            return makeLemmaCommandToSExp(cmd)
-        }
-        case 'make-case': {
-            return makeCaseCommandToSExp(cmd)
-        }
-        case 'metavariables': {
-            return metavariablesCommandToSExp(cmd)
-        }
-        case 'proof-search': {
-            return proofSearchCommandToSExp(cmd)
-        }
-        case 'print-definition': {
-            return printDefinitionCommandToSExp(cmd)
-        }
-        case 'browse-namespace': {
-            return browseNamespaceCommandToSepx(cmd)
-        }
-        case 'apropos': {
-            return aproposCommandToSExp(cmd)
-        }
-        case 'repl-completions': {
-            return replCompletionCommandToSExp(cmd)
-        }
-    }
-}
diff --git a/lib/typings/atom-message-panel.d.ts b/lib/typings/atom-message-panel.d.ts
index c499081..8f73d81 100644
--- a/lib/typings/atom-message-panel.d.ts
+++ b/lib/typings/atom-message-panel.d.ts
@@ -1,10 +1,90 @@
 declare module 'atom-message-panel' {
-    type MessagePanelView = any
+    type MessagePanelViewParams = {
+        title: string
+        /** set to true will allow the title to contains HTML (default is false)
+         */
+        rawTitle?: boolean
+        /**
+         * What should the close button do? hide (default) or destroy
+         */
+        closeMethod?: boolean
+        /**
+         * should the panel attach to the "top", "bottom", "left" or "right" (default is bottom)
+         */
+        position?: 'top' | 'bottom' | 'left' | 'right'
+    }
+
+    interface MessagePanelView {
+        new (params: MessagePanelViewParams): MessagePanelView
+
+        attach(): void
+        show(): void
+        hide(): void
+        clear(): void
+        setTitle(title: string, raw?: boolean): void
+        /**
+         * fold/unfold the panel
+         */
+        toggle(): void
+        /**
+         * unfold the panel
+         */
+        unfold(): void
+        /**
+         * clear the body
+         */
+        clear(): void
+        /**
+         * add a view to the panel
+         */
+        add(view: any): void
+
+        /**
+         * remove a view from the panel
+         */
+        remove(index: number): void
+        /**
+         * get current state informations about your panel
+         */
+        state(): any
+    }
     export const MessagePanelView: MessagePanelView
 
     type PlainMessageView = any
     export const PlainMessageView: PlainMessageView
 
-    type LineMessageView = any
+    type LineMessageViewParams = {
+        /**
+         * your message to the people
+         */
+        message: string
+
+        /**
+         * what line are we talking about?
+         */
+        line: number
+
+        /**
+         * so, was that in some other file? (this is optional)
+         */
+        file?: string
+
+        /**
+         * lets be more specific of what we are talking about (this is optional)
+         */
+        character?: number
+        /**
+         * lets you display a code snippet inside a pre tag (this is optional)
+         */
+        preview?: string
+        /**
+         * adding css classes to your message (this is optional)
+         */
+        className?: string
+    }
+
+    interface LineMessageView {
+        new (params: LineMessageViewParams): LineMessageView
+    }
     export const LineMessageView: LineMessageView
 }
diff --git a/lib/typings/bennu.d.ts b/lib/typings/bennu.d.ts
deleted file mode 100644
index c7b50d1..0000000
--- a/lib/typings/bennu.d.ts
+++ /dev/null
@@ -1,39 +0,0 @@
-declare module 'bennu' {
-    export type Parser<T> = {
-        map: any
-    }
-
-    export type Parse = {
-        always: <T>(t: T) => Parser<T>
-        attempt: any
-        between: any
-        choice: <T>(...choices: Array<Parser<T>>) => Parser<T>
-        either: <T>(l: Parser<T>, r: Parser<T>) => Parser<T>
-        many: any
-        many1: any
-        next: <T, U>(p1: Parser<T>, p2: Parser<U>) => Parser<U>
-        rec: any
-        run: any
-        token: (test: (c: string) => boolean) => any
-    }
-
-    export const parse: Parse
-
-    export type Text = {
-        character: (c: string) => Parser<string>
-        digit: Parser<string>
-        noneOf: any
-        run: any
-        space: Parser<never>
-        string: (s: string) => Parser<string>
-    }
-
-    export const text: Text
-
-    export type Lang = {
-        between: any
-        sepBy: any
-    }
-
-    export const lang: Lang
-}
diff --git a/lib/typings/nu-stream.d.ts b/lib/typings/nu-stream.d.ts
deleted file mode 100644
index ddc52ca..0000000
--- a/lib/typings/nu-stream.d.ts
+++ /dev/null
@@ -1,7 +0,0 @@
-declare module 'nu-stream' {
-    export type Stream = {
-        toArray: any
-    }
-
-    export const stream: Stream
-}
diff --git a/lib/utils/Logger.ts b/lib/utils/Logger.ts
deleted file mode 100644
index be558c8..0000000
--- a/lib/utils/Logger.ts
+++ /dev/null
@@ -1,72 +0,0 @@
-import { appendFile } from 'fs'
-import * as sexpFormatter from '../protocol/sexp-formatter'
-import { SExp } from '../protocol/ide-protocol'
-
-type LogOutput =
-    | { type: 'none' }
-    | { type: 'console' }
-    | { type: 'file'; path: string }
-
-class Logger {
-    logOutput: LogOutput = { type: 'none' }
-
-    logText(str: string): void {
-        switch (this.logOutput.type) {
-            case 'none': {
-                return
-            }
-            case 'console': {
-                console.log(str)
-                return
-            }
-            case 'file': {
-                appendFile(this.logOutput.path, str, (err) => {
-                    if (err) {
-                        throw err
-                    }
-                })
-                return
-            }
-        }
-    }
-
-    logObject(description: string, obj: object): void {
-        switch (this.logOutput.type) {
-            case 'none': {
-                return
-            }
-            case 'console': {
-                console.log(description, obj)
-                return
-            }
-            case 'file': {
-                const output = `=====\n${description}:\n\n${JSON.stringify(
-                    obj,
-                    undefined,
-                    4,
-                )}`
-                appendFile(this.logOutput.path, output, (err) => {
-                    if (err) {
-                        throw err
-                    }
-                })
-                return
-            }
-        }
-    }
-
-    formatCommand(cmd: SExp): string {
-        return sexpFormatter.serialize(cmd)
-    }
-
-    logIncomingCommand(str: string): void {
-        this.logText(`< ${str}\n`)
-    }
-
-    logOutgoingCommand(cmd: any): void {
-        const str = this.formatCommand(cmd)
-        this.logText(`> ${str}`)
-    }
-}
-
-export default new Logger()
diff --git a/lib/utils/dom.ts b/lib/utils/dom.ts
index a080cef..dcc993c 100644
--- a/lib/utils/dom.ts
+++ b/lib/utils/dom.ts
@@ -1,6 +1,9 @@
-export const joinHtmlElements = function (containerElem: any, elems: any) {
+export const joinHtmlElements = function (
+    containerElem: string,
+    elems: Array<Node>,
+) {
     const div = document.createElement(containerElem)
-    elems.forEach((elem: any) => div.appendChild(elem))
+    elems.forEach((elem) => div.appendChild(elem))
     return div
 }
 
diff --git a/lib/utils/highlighter.ts b/lib/utils/highlighter.ts
index c001122..0f6a7e4 100644
--- a/lib/utils/highlighter.ts
+++ b/lib/utils/highlighter.ts
@@ -1,5 +1,6 @@
 import * as Preact from 'preact'
-import Logger from './Logger'
+import { MessageMetadata } from 'idris-ide-client/build/reply'
+import { Decor } from 'idris-ide-client/build/s-exps'
 
 export type HighlightInformation = {
     classes: Array<string>
@@ -7,19 +8,9 @@ export type HighlightInformation = {
     description: string
 }
 
-const highlightInfoListToOb = (list: Array<any>) => {
-    const obj: { [key: string]: any } = {}
-    for (let x of list) {
-        const key = x[0].slice(1)
-        const value = x[1]
-        obj[key] = value
-    }
-    return obj
-}
-
 // Use the right CSS classes, so that we can use the
 // syntax highlighting built into atom.
-const decorToClasses = (decor: string) => {
+const decorToClasses = (decor: Decor | undefined): Array<string> => {
     switch (decor) {
         case ':type':
             return ['syntax--storage', 'syntax--type']
@@ -34,62 +25,56 @@ const decorToClasses = (decor: string) => {
         case ':metavar':
             return ['syntax--constant']
         default:
-            Logger.logText('unknown decor: ' + decor)
-            Logger.logText(
-                'you may want to review the highlighter.coffee script',
-            )
             return []
     }
 }
 
-const highlightWord = (word: string, info: any): HighlightInformation => {
-    const type = info.info.type || ''
-    const doc = info.info['doc-overview'] || ''
+const highlightWord = (
+    word: string,
+    info: MessageMetadata,
+): HighlightInformation => {
+    const type = info.metadata.type || ''
+    const doc = info.metadata.docOverview || ''
 
-    const description = info.info.type != null ? `${type}\n\n${doc}`.trim() : ''
+    const description = type != '' ? `${type}\n\n${doc}`.trim() : ''
 
     return {
-        classes: decorToClasses(info.info.decor).concat('syntax--idris'),
+        classes: decorToClasses(info.metadata.decor).concat('syntax--idris'),
         word,
         description,
     }
 }
 
+type Acc = {
+    position: number
+    text: Array<HighlightInformation>
+}
+const initialAcc: Acc = { position: 0, text: [] }
+
 // Build highlighting information that we can then pass to one
 // of our serializers.
 export const highlight = (
     code: string,
-    highlightingInfo: Array<[number, number, Array<any>]>,
+    highlightingInfo: Array<MessageMetadata>,
 ): Array<HighlightInformation> => {
     const highlighted = highlightingInfo
-        .map(function ([start, length, info]) {
-            return {
-                start,
-                length,
-                info: highlightInfoListToOb(info),
+        .filter((i) => i.metadata.decor != null)
+        .reduce<Acc>(({ position, text }, info) => {
+            const newPosition: number = info.start + info.length
+            const unhighlightedText = {
+                classes: [],
+                word: code.slice(position, info.start),
+                description: '',
             }
-        })
-        .filter((i) => i.info.decor != null)
-        .reduce<[number, Array<HighlightInformation>]>(
-            ([position, text], info) => {
-                const newPosition = info.start + info.length
-                const unhighlightedText: HighlightInformation = {
-                    classes: [],
-                    word: code.slice(position, info.start),
-                    description: '',
-                }
-                const highlightedWord = highlightWord(
-                    code.slice(info.start, newPosition),
-                    info,
-                )
-                const newText = text.concat(unhighlightedText, highlightedWord)
-
-                return [newPosition, newText]
-            },
-            [0, []],
-        )
+            const highlightedWord = highlightWord(
+                code.slice(info.start, newPosition),
+                info,
+            )
+            const newText = text.concat(unhighlightedText, highlightedWord)
+            return { position: newPosition, text: newText }
+        }, initialAcc)
 
-    const [position, text] = highlighted
+    const { position, text } = highlighted
     const rest = {
         classes: [],
         word: code.slice(position),
@@ -97,7 +82,7 @@ export const highlight = (
     }
     const higlightedWords = text.concat(rest)
     return higlightedWords.filter(
-        (higlightedWord: any) => higlightedWord.word !== '',
+        (higlightedWord) => higlightedWord.word !== '',
     )
 }
 
@@ -120,13 +105,13 @@ export const highlightToHtml = (highlights: Array<HighlightInformation>) => {
             return document.createTextNode(word)
         } else {
             const span = document.createElement('span')
-            classes.forEach((c: any) => span.classList.add(c))
+            classes.forEach((c) => span.classList.add(c))
             span.textContent = word
             return span
         }
     })
     const container = document.createElement('span')
-    spans.forEach((span: any) => container.appendChild(span))
+    spans.forEach((span) => container.appendChild(span))
     return container
 }
 
diff --git a/lib/utils/ipkg.ts b/lib/utils/ipkg.ts
index ea34b45..49df9ba 100644
--- a/lib/utils/ipkg.ts
+++ b/lib/utils/ipkg.ts
@@ -1,13 +1,12 @@
+import { readdir, readFile } from 'fs'
+import { promisify } from 'util'
+import { extname, join } from 'path'
 import { Project } from 'atom'
-import * as path from 'path'
-import * as fs from 'fs'
-import * as Rx from 'rx-lite'
-import Logger from './Logger'
 
-type IpkgFile = {
+export type FileInfo = {
     file: string
-    directory: string
     path: string
+    directory: string
     ext: string
 }
 
@@ -17,48 +16,88 @@ export type CompilerOptions = {
     src?: string
 }
 
+export const defaultCompilerOptions: CompilerOptions = {
+    pkgs: [],
+}
+
+/**
+ * Check if two `CompilerOptions` are the same.
+ */
+export function sameCompilerOptions(
+    c1: CompilerOptions,
+    c2: CompilerOptions,
+): boolean {
+    const sameOptions = c1.options === c2.options
+    const sameSrc = c1.src === c2.src
+    const p1 = c1.pkgs
+    const p2 = c2.pkgs
+    const samePkgs =
+        p1.length === p2.length &&
+        p1.every((value, index) => value === p2[index])
+    return sameOptions && sameSrc && samePkgs
+}
+
+const readDirPromise = promisify(readdir)
+const readFilePromise = promisify(readFile)
+
 const optionsRegexp = /opts\s*=\s*\"([^\"]*)\"/
 const sourcedirRegexp = /sourcedir\s*=\s*([a-zA-Z/0-9.]+)/
 const pkgsRegexp = /pkgs\s*=\s*(([a-zA-Z/0-9., -_]+\s{0,1})*)/
 
-// Find all ipkg-files in a directory and returns
-// an observable of an array of files
-export const findIpkgFile = (
-    project: Project,
-): Rx.Observable<Array<IpkgFile>> => {
+/**
+ * Get the project folder from a `Project.
+ */
+export function getProjectFolder(project: Project): string {
     const directories = project.getDirectories()
     const directory = directories[0]
-    let directoryPath: string
     if (directory) {
-        Logger.logText('Project detected')
-        directoryPath = directory.getPath()
+        return directory.getPath()
     } else {
-        Logger.logText('Single file detected')
         const editor: any = atom.workspace.getActivePaneItem()
         const file = editor?.buffer?.file
-        directoryPath = file.getParent().path
+        return file.getParent().path
     }
+}
 
-    const readDir = Rx.Observable.fromNodeCallback(fs.readdir)
-
-    const r = readDir(directoryPath)
-    return r.map((files: any) =>
-        files
+/**
+ * Find an iPKG file in the project directory.
+ * Uses the first one it finds right now.
+ */
+export async function findIpkgFile(
+    projectDirectory: string,
+): Promise<FileInfo | null> {
+    try {
+        const files = await readDirPromise(projectDirectory)
+        const ipkgFiles = files
             .map(
-                (file: string): IpkgFile => ({
-                    file,
-                    directory: directoryPath,
-                    path: path.join(directoryPath, file),
-                    ext: path.extname(file),
-                }),
+                (file): FileInfo => {
+                    return {
+                        file,
+                        path: join(projectDirectory, file),
+                        directory: projectDirectory,
+                        ext: extname(file),
+                    }
+                },
             )
-            .filter((file: IpkgFile) => file.ext === '.ipkg'),
-    )
+            .filter((file) => file.ext === '.ipkg')
+        if (ipkgFiles.length > 0) {
+            return ipkgFiles[0]
+        } else {
+            return null
+        }
+    } catch {
+        return null
+    }
 }
 
-const parseIpkgFile = (fileInfo: any) => (
+/**
+ * Parse the important parts of an iPKG file
+ * into `CompilerOptions`
+ */
+export function parseIpkgFile(
+    fileInfo: FileInfo,
     fileContents: string,
-): CompilerOptions => {
+): CompilerOptions {
     const optionsMatches = fileContents.match(optionsRegexp)
     const sourcedirMatches = fileContents.match(sourcedirRegexp)
     const pkgsMatches = fileContents.match(pkgsRegexp)
@@ -70,29 +109,58 @@ const parseIpkgFile = (fileInfo: any) => (
         : []
 
     const src = sourcedirMatches
-        ? path.join(fileInfo.directory, sourcedirMatches[1])
+        ? join(fileInfo.directory, sourcedirMatches[1])
         : fileInfo.directory
 
     return { options, pkgs, src }
 }
 
-export const readIpkgFile = (ipkgFile: any): Rx.Observable<string> => {
-    const readFile: any = Rx.Observable.fromNodeCallback(fs.readFile)
-    return readFile(ipkgFile.path, { encoding: 'utf8' })
+/**
+ * Try to find the iPKG file and parse the important bits out
+ * from a `Project`.
+ */
+export async function findAndReadIpkgFile(
+    project: Project,
+): Promise<CompilerOptions | null> {
+    const projectFolder = getProjectFolder(project)
+    const ipkgFile = await findIpkgFile(projectFolder)
+    if (ipkgFile) {
+        const fileContents = await readFilePromise(ipkgFile.path, {
+            encoding: 'utf8',
+        })
+        return parseIpkgFile(ipkgFile, fileContents)
+    } else {
+        return null
+    }
 }
 
-// Find the ipkg file in the top directory of the project and return
-// the compiler options in it.
-export const compilerOptions = (project: Project) => {
-    const ipkgFilesObserver = findIpkgFile(project) as any
-    return ipkgFilesObserver
-        .flatMap((ipkgFiles: any) => {
-            if (ipkgFiles.length) {
-                const ipkgFile = ipkgFiles[0]
-                return readIpkgFile(ipkgFile).map(parseIpkgFile(ipkgFile))
-            } else {
-                return Rx.Observable.return({})
-            }
-        })
-        .catch(() => Rx.Observable.return({}))
+/**
+ * Convert `CompilerOptions` to command line parameters
+ * understood by the idris compiler.
+ * @param compilerOptions
+ * @param tabLength
+ */
+export function compilerOptionsToFlags(
+    compilerOptions: CompilerOptions,
+    tabLength: number,
+): Array<string> {
+    let ipkgOptions = compilerOptions.options
+        ? compilerOptions.options.split(' ')
+        : []
+
+    const configParams = [
+        '--ide-mode',
+        '--indent-with=' + tabLength,
+        '--indent-clause=' + tabLength,
+    ]
+
+    const packageTuples = compilerOptions.pkgs.map((p) => ['-p', p])
+
+    const emptyStringArray: Array<string> = []
+    const pkgs: Array<string> = emptyStringArray.concat.apply(
+        emptyStringArray,
+        packageTuples,
+    )
+    const parameters = configParams.concat(pkgs, ipkgOptions)
+    return parameters
 }
diff --git a/lib/utils/js.ts b/lib/utils/js.ts
deleted file mode 100644
index 5c0d13c..0000000
--- a/lib/utils/js.ts
+++ /dev/null
@@ -1,3 +0,0 @@
-// slow method to compare objects.
-export const objectEqual = (a: any, b: any) =>
-    JSON.stringify(a) === JSON.stringify(b)
diff --git a/lib/utils/parse.ts b/lib/utils/parse.ts
deleted file mode 100644
index 8d6a6ad..0000000
--- a/lib/utils/parse.ts
+++ /dev/null
@@ -1,56 +0,0 @@
-import { parse, text, lang } from 'bennu'
-import { stream } from 'nu-stream'
-
-// this module defines the parse required to deal with S-Expressions
-// as used for the communication with the Idris IDE
-
-const streamToString = (s: any): string => stream.toArray(s).join('')
-
-// bool
-export const trueP = parse.next(text.string(':True'), parse.always(true))
-export const falseP = parse.next(text.string(':False'), parse.always(false))
-const boolP = parse.either(trueP, falseP)
-
-// integer
-export const integerP = parse
-    .many1(text.digit)
-    .map(streamToString)
-    .map((s: string) => parseInt(s, 10))
-
-// string
-const quoteP = text.character('"')
-const escapedP = parse.choice(
-    parse.next(text.character('\\'), parse.always('\\')),
-    parse.next(text.character('"'), parse.always('"')),
-)
-const stringLetterP = parse.token((c: string) => c !== '"' && c !== '\\')
-const stringEscapeP = parse.attempt(parse.next(text.character('\\'), escapedP))
-const stringBackslashP = text.character('\\')
-export const stringCharP = parse.choice(
-    stringLetterP,
-    stringEscapeP,
-    stringBackslashP,
-)
-export const stringP = lang
-    .between(quoteP, quoteP, parse.many(stringCharP))
-    .map(streamToString)
-
-// symbol
-const symbolStartP = text.character(':')
-const symbolChar = text.noneOf(' )')
-export const symbolP = parse
-    .next(symbolStartP, parse.many(symbolChar))
-    .map(streamToString)
-    .map((symbol: string) => `:${symbol}`)
-
-// sexp
-const openP = text.character('(')
-const closeP = text.character(')')
-const sexpP = parse.rec((self: any) => {
-    const choices = parse.choice(boolP, integerP, stringP, symbolP, self)
-    return lang
-        .between(openP, closeP, lang.sepBy(text.space, choices))
-        .map(stream.toArray)
-})
-
-export const parseCommand = (input: string) => parse.run(sexpP, input)
diff --git a/lib/views/apropos-view.tsx b/lib/views/apropos-view.tsx
index 7c30f37..74a94c0 100644
--- a/lib/views/apropos-view.tsx
+++ b/lib/views/apropos-view.tsx
@@ -1,44 +1,25 @@
 import * as Preact from 'preact'
 import { useState, StateUpdater } from 'preact/hooks'
 import * as highlighter from '../utils/highlighter'
-import * as Rx from 'rx-lite'
 import { fontOptions } from '../utils/dom'
 import { IdrisController } from '../idris-controller'
-import { IdrisModel } from '../idris-model'
 import { HighlightInformation } from '../utils/highlighter'
+import { IdrisClient, FinalReply } from 'idris-ide-client'
 
 const styles = fontOptions()
 
 const ask = (
-    model: IdrisModel,
+    client: IdrisClient,
     question: string,
     setAnswer: StateUpdater<Array<HighlightInformation>>,
 ) => {
-    model
-        .apropos(question)
-        .map((e: any): {
-            code: string
-            highlightInfo: Array<[number, number, Array<any>]>
-        } => ({
-            code: e.msg[0],
-            highlightInfo: e.msg[1],
-        }))
-        .catch((e: any) =>
-            Rx.Observable.just({
-                code: e.message,
-                highlightInfo: e.highlightInformation,
-            }),
-        )
-        .subscribe(
-            ({ code, highlightInfo }) => {
-                const answer = highlighter.highlight(code, highlightInfo)
-                setAnswer(answer)
-            },
-            (err) =>
-                setAnswer([
-                    { word: err.message, classes: [], description: '' },
-                ]),
-        )
+    client.apropos(question).then((reply: FinalReply.Apropos) => {
+        if ('ok' in reply) {
+            setAnswer(highlighter.highlight(reply.ok.docs, reply.ok.metadata))
+        } else {
+            setAnswer(highlighter.highlight(reply.err, []))
+        }
+    })
 }
 
 type AnswerProps = { highlightInfo: Array<HighlightInformation> }
@@ -52,10 +33,10 @@ const Answer: Preact.FunctionComponent<AnswerProps> = (props) => {
     )
 }
 
-type AproposProps = { model: IdrisModel }
+type AproposProps = { client: IdrisClient }
 
 const Apropos: Preact.FunctionComponent<AproposProps> = (props) => {
-    const { model } = props
+    const { client } = props
     const [input, setInput] = useState<string>('')
     const [answer, setAnswer] = useState<Array<HighlightInformation>>([])
 
@@ -69,7 +50,7 @@ const Apropos: Preact.FunctionComponent<AproposProps> = (props) => {
                 }}
                 onKeyPress={(e) => {
                     if (e.keyCode === 13) {
-                        ask(model, input, setAnswer)
+                        ask(client, input, setAnswer)
                     }
                 }}
             >
@@ -88,8 +69,8 @@ export class AproposView {
     constructor(params: { controller: IdrisController }) {
         const hostElement = this[0]
 
-        const { model } = params.controller
+        const { client } = params.controller
 
-        Preact.render(<Apropos model={model} />, hostElement)
+        Preact.render(<Apropos client={client} />, hostElement)
     }
 }
diff --git a/lib/views/browse-namespace.tsx b/lib/views/browse-namespace.tsx
new file mode 100644
index 0000000..54f5a2a
--- /dev/null
+++ b/lib/views/browse-namespace.tsx
@@ -0,0 +1,73 @@
+import * as Preact from 'preact'
+import { MessageMetadata } from 'idris-ide-client/build/reply'
+import { highlight, highlightToPreact } from '../utils/highlighter'
+import { fontOptions } from '../utils/dom'
+
+export type Declaration = {
+    name: string
+    metadata: Array<MessageMetadata>
+}
+
+type SubModulesProps = {
+    subModules: Array<string>
+}
+
+const SubModulesView: Preact.FunctionComponent<SubModulesProps> = (
+    props: SubModulesProps,
+) => {
+    const { subModules } = props
+    return (
+        <div>
+            <h3>Submodules</h3>
+            {subModules.map((subModule) => (
+                <div>{subModule}</div>
+            ))}
+        </div>
+    )
+}
+
+type DeclarationsProps = { declarations: Array<Declaration> }
+
+const DeclarationsView: Preact.FunctionComponent<DeclarationsProps> = (
+    props: DeclarationsProps,
+) => {
+    const { declarations } = props
+    return (
+        <div>
+            <h3>Declarations</h3>
+            {declarations.map((declaration) => {
+                const highlighted = highlightToPreact(
+                    highlight(declaration.name, declaration.metadata),
+                )
+                return <div>{highlighted}</div>
+            })}
+        </div>
+    )
+}
+
+type BrowseNamespaceProps = {
+    subModules: Array<string>
+    declarations: Array<Declaration>
+}
+
+const BrowseNamespace: Preact.FunctionComponent<BrowseNamespaceProps> = (
+    props,
+) => {
+    const { subModules, declarations } = props
+
+    return (
+        <pre style={fontOptions()}>
+            <SubModulesView subModules={subModules} />
+            <DeclarationsView declarations={declarations} />
+        </pre>
+    )
+}
+
+export const browseNamespaceView = (
+    props: BrowseNamespaceProps,
+): HTMLElement => {
+    const hostElement = document.createElement('div')
+
+    Preact.render(<BrowseNamespace {...props} />, hostElement)
+    return hostElement
+}
diff --git a/lib/views/holes-view.ts b/lib/views/holes-view.ts
index 32e56b9..0c578a9 100644
--- a/lib/views/holes-view.ts
+++ b/lib/views/holes-view.ts
@@ -1,12 +1,20 @@
+import { FinalReply } from 'idris-ide-client'
 import * as highlighter from '../utils/highlighter'
 import { createCodeElement, joinHtmlElements } from '../utils/dom'
+import { MessageMetadata } from 'idris-ide-client/build/reply'
 
 const textNode = (text: string): Text => document.createTextNode(text)
 
+type Metavariable = {
+    name: string
+    type: string
+    metadata: Array<MessageMetadata>
+}
+
 export class HolesViewClass extends HTMLElement {
     holesContainer: HTMLPreElement | undefined
 
-    initialize(holes: any): void {
+    initialize(holes: FinalReply.Metavariables): void {
         this.classList.add('idris-panel')
         this.holesContainer = createCodeElement()
         this.holesContainer.classList.add('idris-mode')
@@ -17,56 +25,59 @@ export class HolesViewClass extends HTMLElement {
         this.showHoles(holes)
     }
 
-    showHoles(holes: any): void {
+    showHoles(holes: FinalReply.Metavariables): void {
         this.holesContainer?.appendChild(this.prettyprintHoles(holes))
     }
 
-    prettyprintHoles(holes: any) {
-        const html = holes.map(
-            ([name, premises, conclusion]: [string, any, any]) => {
-                return this.prettyprintHole(name, premises, conclusion)
-            },
-        )
+    prettyprintHoles(holes: FinalReply.Metavariables) {
+        const html = holes.ok.map((metavariable) => {
+            return this.prettyprintHole(
+                metavariable.metavariable,
+                metavariable.scope,
+            )
+        })
         return joinHtmlElements('div', html)
     }
 
-    prettyprintHole(name: string, premises: any, conclusion: any) {
+    prettyprintHole(metavariable: Metavariable, premises: Array<Metavariable>) {
         const prettyPremises = this.prettyprintPremises(premises)
-        const prettyConclusion: any = this.prettyprintConclusion(
-            name,
-            conclusion,
-        )
+        const prettyConclusion = this.prettyprintConclusion(metavariable)
 
-        const hole = joinHtmlElements(
-            'div',
-            [textNode(`${name}`)].concat(prettyPremises, prettyConclusion),
-        )
+        const children: Array<HTMLElement | Text> = [
+            textNode(`${name}`),
+            prettyPremises,
+            ...prettyConclusion,
+        ]
+
+        const hole = joinHtmlElements('div', children)
         hole.classList.add('idris')
         hole.classList.add('idris-hole')
         return hole
     }
 
-    prettyprintPremises(premises: any) {
-        const html = premises.map(
-            ([name, type, highlightInformation]: [string, any, any]) => {
-                const highlight = highlighter.highlight(
-                    type,
-                    highlightInformation,
-                )
-                type = highlighter.highlightToHtml(highlight)
-                return joinHtmlElements(
-                    'div',
-                    [textNode(`    ${name} : `)].concat(type),
-                )
-            },
-        )
+    prettyprintPremises(premises: Array<Metavariable>) {
+        const html = premises.map((premise) => {
+            const highlight = highlighter.highlight(
+                premise.type,
+                premise.metadata,
+            )
+            const type = highlighter.highlightToHtml(highlight)
+            return joinHtmlElements('div', [
+                textNode(`    ${premise.name} : `),
+                type,
+            ])
+        })
         return joinHtmlElements('div', html)
     }
 
-    prettyprintConclusion(name: string, [type, highlightInformation]: any) {
-        const highlight = highlighter.highlight(type, highlightInformation)
+    prettyprintConclusion(metavariable: Metavariable) {
+        const highlight = highlighter.highlight(
+            metavariable.type,
+            metavariable.metadata,
+        )
         const highlightedConclusion = highlighter.highlightToHtml(highlight)
-        const dividerLength = `${name} : ${type}`.length
+        const dividerLength = `${metavariable.name} : ${metavariable.type}`
+            .length
         var divider = ''
         for (var i = 0; i < dividerLength; i++) {
             divider += '-'
@@ -75,7 +86,7 @@ export class HolesViewClass extends HTMLElement {
         return [
             textNode(divider),
             document.createElement('br'),
-            textNode(`${name} : `),
+            textNode(`${metavariable.name} : `),
             highlightedConclusion,
         ]
     }
diff --git a/lib/views/information-view.ts b/lib/views/information-view.ts
index fd884b5..b087fe6 100644
--- a/lib/views/information-view.ts
+++ b/lib/views/information-view.ts
@@ -1,26 +1,19 @@
 import * as highlighter from '../utils/highlighter'
 import * as dom from '../utils/dom'
+import { MessageMetadata } from 'idris-ide-client/build/reply'
 
 export class InformationViewClass extends HTMLElement {
-    obligation: any
-    highlightingInfo: any
-    text: any
-
-    initialize(params: any) {
+    initialize(content: string, metadata?: Array<MessageMetadata>) {
         this.classList.add('idris-panel')
-        this.obligation = params.obligation
-        this.highlightingInfo = params.highlightingInfo
-        if (this.highlightingInfo != null) {
-            const highlighting = highlighter.highlight(
-                this.obligation,
-                this.highlightingInfo,
-            )
+
+        if (metadata != null) {
+            const highlighting = highlighter.highlight(content, metadata)
             const info = highlighter.highlightToHtml(highlighting)
             const pre = dom.createCodeElement()
             pre.appendChild(info)
             return this.appendChild(pre)
         } else {
-            return this.text(this.obligation)
+            return this.append(content)
         }
     }
 }
diff --git a/lib/views/repl-view.tsx b/lib/views/repl-view.tsx
index 0806bb1..6a9ca91 100644
--- a/lib/views/repl-view.tsx
+++ b/lib/views/repl-view.tsx
@@ -1,10 +1,10 @@
 import * as Preact from 'preact'
 import { useState, StateUpdater } from 'preact/hooks'
-import { IdrisModel } from '../idris-model'
 import { HighlightInformation } from '../utils/highlighter'
 import * as highlighter from '../utils/highlighter'
-import * as Rx from 'rx-lite'
 import { fontOptions } from '../utils/dom'
+import { IdrisController } from '../idris-controller'
+import { IdrisClient, FinalReply } from 'idris-ide-client'
 
 const styles = fontOptions()
 
@@ -23,41 +23,37 @@ type ReplLineError = {
 type ReplLine = ReplLineSuccess | ReplLineError
 
 const ask = (
-    model: IdrisModel,
+    client: IdrisClient,
     question: string,
     lines: Array<ReplLine>,
     setLines: StateUpdater<Array<ReplLine>>,
 ) => {
     const escapedLine = question.replace(/"/g, '\\"')
-    // append a space to trick the formatter, so that it wont turn
-    // the input into a symbol
-    model
-        .interpret(`${escapedLine} `)
-        .map(
-            (e: any): ReplLine => ({
-                type: 'success',
-                question,
-                answer: highlighter.highlight(e.msg[0], e.msg[1]),
-            }),
-        )
-        .catch((e: any): any => {
-            const errorAnswer: ReplLineError = {
-                type: 'error',
-                question,
-                answer: highlighter.highlight(
-                    e.message,
-                    e.highlightInformation,
-                ),
-            }
-            const ob = Rx.Observable.just(errorAnswer)
-            return ob
-        })
-        .subscribe(
-            (answer: ReplLine) => {
-                setLines(lines.concat([answer]))
+    client
+        .interpret(escapedLine)
+        .then(
+            (reply: FinalReply.Interpret): ReplLine => {
+                if ('ok' in reply) {
+                    return {
+                        type: 'success',
+                        question,
+                        answer: highlighter.highlight(
+                            reply.ok.result,
+                            reply.ok.metadata,
+                        ),
+                    }
+                } else
+                    return {
+                        type: 'error',
+                        question,
+                        answer: highlighter.highlight(
+                            reply.err.message,
+                            reply.err.metadata,
+                        ),
+                    }
             },
-            (err) => console.log(err),
         )
+        .then((answer) => setLines(lines.concat([answer])))
 }
 
 const SuccessAnswer: Preact.FunctionComponent<{
@@ -104,10 +100,10 @@ const Line: Preact.FunctionComponent<ReplLine> = (props) => {
     )
 }
 
-type ReplProps = { model: IdrisModel }
+type ReplProps = { client: IdrisClient }
 
 const Repl: Preact.FunctionComponent<ReplProps> = (props) => {
-    const { model } = props
+    const { client } = props
 
     const [input, setInput] = useState<string>('')
     const [lines, setLines] = useState<Array<ReplLine>>([])
@@ -122,7 +118,7 @@ const Repl: Preact.FunctionComponent<ReplProps> = (props) => {
                 }}
                 onKeyPress={(e) => {
                     if (e.keyCode === 13) {
-                        ask(model, input, lines, setLines)
+                        ask(client, input, lines, setLines)
                     }
                 }}
             ></input>
@@ -143,11 +139,11 @@ const Repl: Preact.FunctionComponent<ReplProps> = (props) => {
 export class REPLView {
     0: HTMLDivElement = document.createElement('div')
 
-    constructor(params: any) {
+    constructor(params: { controller: IdrisController }) {
         const hostElement = this[0]
 
-        const { model } = params.controller
+        const { client } = params.controller
 
-        Preact.render(<Repl model={model} />, hostElement)
+        Preact.render(<Repl client={client} />, hostElement)
     }
 }
diff --git a/package-lock.json b/package-lock.json
index bbaf785..c66d7e7 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -19,35 +19,10 @@
       "integrity": "sha512-FAYBGwC+W6F9+huFIDtn43cpy7+SzG+atzRiTfdp3inUKL2hXnd4rG8hylJLIh4+hqrQy1P17kvJByE/z825hA==",
       "dev": true
     },
-    "@types/rx-core": {
-      "version": "4.0.3",
-      "resolved": "https://registry.npmjs.org/@types/rx-core/-/rx-core-4.0.3.tgz",
-      "integrity": "sha1-CzNUsSOM7b4rdPYybxOdvHpZHWA=",
-      "dev": true
-    },
-    "@types/rx-core-binding": {
-      "version": "4.0.4",
-      "resolved": "https://registry.npmjs.org/@types/rx-core-binding/-/rx-core-binding-4.0.4.tgz",
-      "integrity": "sha512-5pkfxnC4w810LqBPUwP5bg7SFR/USwhMSaAeZQQbEHeBp57pjKXRlXmqpMrLJB4y1oglR/c2502853uN0I+DAQ==",
-      "dev": true,
-      "requires": {
-        "@types/rx-core": "*"
-      }
-    },
-    "@types/rx-lite": {
-      "version": "4.0.6",
-      "resolved": "https://registry.npmjs.org/@types/rx-lite/-/rx-lite-4.0.6.tgz",
-      "integrity": "sha512-oYiDrFIcor9zDm0VDUca1UbROiMYBxMLMaM6qzz4ADAfOmA9r1dYEcAFH+2fsPI5BCCjPvV9pWC3X3flbrvs7w==",
-      "dev": true,
-      "requires": {
-        "@types/rx-core": "*",
-        "@types/rx-core-binding": "*"
-      }
-    },
     "atom-message-panel": {
-      "version": "1.3.0",
-      "resolved": "https://registry.npmjs.org/atom-message-panel/-/atom-message-panel-1.3.0.tgz",
-      "integrity": "sha1-BOICKVQHZrzTVlVdq/qY1b7dMTw=",
+      "version": "1.3.1",
+      "resolved": "https://registry.npmjs.org/atom-message-panel/-/atom-message-panel-1.3.1.tgz",
+      "integrity": "sha512-nLi19faNBl/kabrf6itBkHcLrnpUeiGbpda+dHufAODKH+I+odoPRCxx7EZ+mCHEsBMhHNXxLWOLA+Mm9pumbA==",
       "requires": {
         "atom-space-pen-views": "^2.2.0"
       }
@@ -66,15 +41,6 @@
       "resolved": "https://registry.npmjs.org/atom-ts-transpiler/-/atom-ts-transpiler-1.5.2.tgz",
       "integrity": "sha512-X1Ii+whd+9MuwzV6nXyqpAOq886PH70YcCDDXgFGwkkfMChJndbedBAPUhnp9JqgoktiY0JLkOMmFsdBwuf70g=="
     },
-    "bennu": {
-      "version": "17.3.0",
-      "resolved": "https://registry.npmjs.org/bennu/-/bennu-17.3.0.tgz",
-      "integrity": "sha1-7hMvJam7aMyMnV4PsRP+4SAoydM=",
-      "requires": {
-        "nu-stream": ">=3.1.0",
-        "seshet": "0.1.x"
-      }
-    },
     "d": {
       "version": "0.1.1",
       "resolved": "https://registry.npmjs.org/d/-/d-0.1.1.tgz",
@@ -95,12 +61,12 @@
       }
     },
     "es5-ext": {
-      "version": "0.10.52",
-      "resolved": "https://registry.npmjs.org/es5-ext/-/es5-ext-0.10.52.tgz",
-      "integrity": "sha512-bWCbE9fbpYQY4CU6hJbJ1vSz70EClMlDgJ7BmwI+zEJhxrwjesZRPglGJlsZhu0334U3hI+gaspwksH9IGD6ag==",
+      "version": "0.10.53",
+      "resolved": "https://registry.npmjs.org/es5-ext/-/es5-ext-0.10.53.tgz",
+      "integrity": "sha512-Xs2Stw6NiNHWypzRTY1MtaG/uJlwCk8kH81920ma8mvN8Xq1gsfhZvpkImLQArw8AHnv8MT2I45J3c0R8slE+Q==",
       "requires": {
         "es6-iterator": "~2.0.3",
-        "es6-symbol": "~3.1.2",
+        "es6-symbol": "~3.1.3",
         "next-tick": "~1.0.0"
       },
       "dependencies": {
@@ -142,17 +108,15 @@
         "d": "~0.1.1",
         "es5-ext": "~0.10.5",
         "es6-symbol": "~2.0.1"
-      },
-      "dependencies": {
-        "es6-symbol": {
-          "version": "2.0.1",
-          "resolved": "https://registry.npmjs.org/es6-symbol/-/es6-symbol-2.0.1.tgz",
-          "integrity": "sha1-dhtcZ8/U8dGK+yNPaR1nhoLLO/M=",
-          "requires": {
-            "d": "~0.1.1",
-            "es5-ext": "~0.10.5"
-          }
-        }
+      }
+    },
+    "es6-symbol": {
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/es6-symbol/-/es6-symbol-2.0.1.tgz",
+      "integrity": "sha1-dhtcZ8/U8dGK+yNPaR1nhoLLO/M=",
+      "requires": {
+        "d": "~0.1.1",
+        "es5-ext": "~0.10.5"
       }
     },
     "es6-weak-map": {
@@ -164,23 +128,12 @@
         "es5-ext": "~0.10.6",
         "es6-iterator": "~0.1.3",
         "es6-symbol": "~2.0.1"
-      },
-      "dependencies": {
-        "es6-symbol": {
-          "version": "2.0.1",
-          "resolved": "https://registry.npmjs.org/es6-symbol/-/es6-symbol-2.0.1.tgz",
-          "integrity": "sha1-dhtcZ8/U8dGK+yNPaR1nhoLLO/M=",
-          "requires": {
-            "d": "~0.1.1",
-            "es5-ext": "~0.10.5"
-          }
-        }
       }
     },
     "ext": {
-      "version": "1.1.2",
-      "resolved": "https://registry.npmjs.org/ext/-/ext-1.1.2.tgz",
-      "integrity": "sha512-/KLjJdTNyDepCihrk4HQt57nAE1IRCEo5jUt+WgWGCr1oARhibDvmI2DMcSNWood1T9AUWwq+jaV1wvRqaXfnA==",
+      "version": "1.4.0",
+      "resolved": "https://registry.npmjs.org/ext/-/ext-1.4.0.tgz",
+      "integrity": "sha512-Key5NIsUxdqKg3vIsdw9dSuXpPCQ297y6wBjL30edxwPgt2E44WcWBZey/ZvUc6sERLTxKdyCu4gZFmUbk1Q7A==",
       "requires": {
         "type": "^2.0.0"
       },
@@ -205,6 +158,11 @@
         "emissary": "^1.2.0"
       }
     },
+    "idris-ide-client": {
+      "version": "0.1.3",
+      "resolved": "https://registry.npmjs.org/idris-ide-client/-/idris-ide-client-0.1.3.tgz",
+      "integrity": "sha512-eJyL7l7r7LJwYY4HqC38XPi0/zZPeHdXDkPqBQLubESFlcXxZMTklzO54H39HemOMnQe5Ir8dYmSMjcjxYXfEg=="
+    },
     "jquery": {
       "version": "2.1.4",
       "resolved": "https://registry.npmjs.org/jquery/-/jquery-2.1.4.tgz",
@@ -220,15 +178,10 @@
       "resolved": "https://registry.npmjs.org/next-tick/-/next-tick-1.0.0.tgz",
       "integrity": "sha1-yobR/ogoFpsBICCOPchCS524NCw="
     },
-    "nu-stream": {
-      "version": "3.3.1",
-      "resolved": "https://registry.npmjs.org/nu-stream/-/nu-stream-3.3.1.tgz",
-      "integrity": "sha1-2atQN7/QDIbna74oaGcnBjuRs68="
-    },
     "preact": {
-      "version": "10.4.4",
-      "resolved": "https://registry.npmjs.org/preact/-/preact-10.4.4.tgz",
-      "integrity": "sha512-EaTJrerceyAPatQ+vfnadoopsMBZAOY7ak9ogVdUi5xbpR8SoHgtLryXnW+4mQOwt21icqoVR1brkU2dq7pEBA=="
+      "version": "10.4.5",
+      "resolved": "https://registry.npmjs.org/preact/-/preact-10.4.5.tgz",
+      "integrity": "sha512-/GyQOM44xNbM1nx1NWWdEO9RFjOVl3Ji6HTnEP+y9OkfyvJDHXnWJPQnuknrslzu5lZfAtFavS8gka91fbFAPg=="
     },
     "prettier": {
       "version": "2.0.5",
@@ -245,16 +198,6 @@
         "mixto": "1.x"
       }
     },
-    "rx-lite": {
-      "version": "4.0.8",
-      "resolved": "https://registry.npmjs.org/rx-lite/-/rx-lite-4.0.8.tgz",
-      "integrity": "sha1-Cx4Rr4vESDbwSmQH6S2kJGe3lEQ="
-    },
-    "seshet": {
-      "version": "0.1.0",
-      "resolved": "https://registry.npmjs.org/seshet/-/seshet-0.1.0.tgz",
-      "integrity": "sha1-8L517ujomfU47nAB+tJux/52VgY="
-    },
     "space-pen": {
       "version": "5.1.2",
       "resolved": "https://registry.npmjs.org/space-pen/-/space-pen-5.1.2.tgz",
@@ -266,9 +209,9 @@
       }
     },
     "tslib": {
-      "version": "1.11.1",
-      "resolved": "https://registry.npmjs.org/tslib/-/tslib-1.11.1.tgz",
-      "integrity": "sha512-aZW88SY8kQbU7gpV19lN24LtXh/yD4ZZg6qieAJDDg+YBsJcSmLGK9QpnUjAKVG/xefmvJGd1WUmfpT/g6AJGA=="
+      "version": "2.0.0",
+      "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.0.0.tgz",
+      "integrity": "sha512-lTqkx847PI7xEDYJntxZH89L2/aXInsyF2luSafe/+0fHOMjlBNXdH6th7f70qxLDhul7KZK0zC8V5ZIyHl0/g=="
     },
     "type": {
       "version": "1.2.0",
@@ -276,14 +219,14 @@
       "integrity": "sha512-+5nt5AAniqsCnu2cEQQdpzCAh33kVx8n0VoFidKpB1dVVLAN/F+bgVOqOJqOnEnrhp222clB5p3vUlD+1QAnfg=="
     },
     "typescript": {
-      "version": "3.9.2",
-      "resolved": "https://registry.npmjs.org/typescript/-/typescript-3.9.2.tgz",
-      "integrity": "sha512-q2ktq4n/uLuNNShyayit+DTobV2ApPEo/6so68JaD5ojvc/6GClBipedB9zNWYxRSAlZXAe405Rlijzl6qDiSw=="
+      "version": "3.9.6",
+      "resolved": "https://registry.npmjs.org/typescript/-/typescript-3.9.6.tgz",
+      "integrity": "sha512-Pspx3oKAPJtjNwE92YS05HQoY7z2SFyOpHo9MqJor3BXAGNaPUs83CuVp9VISFkSjyRfiTpmKuAYGJB7S7hOxw=="
     },
     "underscore": {
-      "version": "1.9.1",
-      "resolved": "https://registry.npmjs.org/underscore/-/underscore-1.9.1.tgz",
-      "integrity": "sha512-5/4etnCkd9c8gwgowi5/om/mYO5ajCaOgdzj/oW+0eQV9WxKBDZw5+ycmKmeaTXjInS/W0BzpGLo2xR2aBwZdg=="
+      "version": "1.10.2",
+      "resolved": "https://registry.npmjs.org/underscore/-/underscore-1.10.2.tgz",
+      "integrity": "sha512-N4P+Q/BuyuEKFJ43B9gYuOj4TQUHXX+j2FqguVOpjkssLUUrnJofCcBccJSCoeturDoZU6GorDTHSvUDlSQbTg=="
     },
     "underscore-plus": {
       "version": "1.7.0",
diff --git a/package.json b/package.json
index fa5ff40..2c68000 100644
--- a/package.json
+++ b/package.json
@@ -7,7 +7,7 @@
     "repository": "https://github.com/idris-hackers/atom-language-idris",
     "license": "MIT",
     "scripts": {
-        "build": "tsc -p ./lib"
+        "build": "tsc -p ."
     },
     "engines": {
         "atom": ">=1.31.0"
@@ -77,18 +77,15 @@
         }
     ],
     "dependencies": {
-        "atom-message-panel": "^1.3.0",
-        "atom-ts-transpiler": "^1.5.2",
-        "bennu": "17.3.0",
-        "nu-stream": "3.3.1",
-        "preact": "10.4.4",
-        "rx-lite": "4.0.8",
-        "tslib": "1.11.1",
-        "typescript": "3.9.2"
+        "atom-message-panel": "1.3.1",
+        "atom-ts-transpiler": "1.5.2",
+        "preact": "10.4.5",
+        "idris-ide-client": "0.1.3",
+        "tslib": "2.0.0",
+        "typescript": "3.9.6"
     },
     "devDependencies": {
         "@types/atom": "1.40.4",
-        "@types/rx-lite": "4.0.6",
         "prettier": "2.0.5"
     }
 }
diff --git a/spec/parse-spec.coffee b/spec/parse-spec.coffee
deleted file mode 100644
index 226132f..0000000
--- a/spec/parse-spec.coffee
+++ /dev/null
@@ -1,138 +0,0 @@
-sexpFormatter = require '../lib/utils/sexp-formatter'
-parse = require '../lib/utils/parse'
-runP = require('bennu').parse.run
-
-test1 = "(:protocol-version 1 0)"
-list1 = [':protocol-version', 1, 0]
-
-test2 = "(:set-prompt \"*C:\\Programming\\Idris\\Start\\hello\" 1)"
-list2 = [":set-prompt", "*C:\\Programming\\Idris\\Start\\hello", 1]
-
-test3 = "(:return (:ok ()) 5)"
-list3 = [":return", [":ok", []], 5]
-
-test4 = """(:return (:ok "Main.a : Nat" ((0 6 ((:name "Main.a") (:implicit :False) (:decor :function) (:doc-overview "") (:type "Nat"))) (9 3 ((:name "Prelude.Nat.Nat") (:implicit :False) (:decor :type) (:doc-overview "Unary natural numbers") (:type "Type"))) (9 3 ((:tt-term "AAAAAAAAAAAAAwAAAAAACAAAAQyZWx1ZGU="))))) 2)"""
-list4 =
-  [
-    ":return",
-    [
-      ":ok",
-      "Main.a : Nat",
-      [
-        [
-          0,
-          6,
-          [
-            [":name", "Main.a"],
-            [":implicit", false],
-            [":decor", ":function"],
-            [":doc-overview", ""],
-            [":type", "Nat"]
-          ]
-        ],
-        [
-          9,
-          3,
-          [
-            [":name", "Prelude.Nat.Nat"],
-            [":implicit", false],
-            [":decor", ":type"],
-            [":doc-overview", "Unary natural numbers"]
-            [":type", "Type"]
-          ]
-        ],
-        [
-          9,
-          3,
-          [
-            [
-              ":tt-term", "AAAAAAAAAAAAAwAAAAAACAAAAQyZWx1ZGU="
-            ]
-          ]
-        ]
-      ]
-    ],
-    2
-  ]
-
-test5 = """(:return (:ok "\\"Z\\" : String" ((0 3 ((:name "\\"Z\\""))))) 5)"""
-list5 =
-  [
-    ":return"
-    [
-      ":ok"
-      '"Z" : String'
-      [
-        [
-          0
-          3
-          [
-            [
-              ":name"
-              '"Z"'
-            ]
-          ]
-        ]
-      ]
-    ]
-    5
-  ]
-
-test6 = """(:return (:ok "\\\\__pi_arg => \\\\__pi_arg1 => (__pi_arg1)") 6)"""
-list6 =
-  [
-    ":return"
-    [
-      ":ok"
-      "\\__pi_arg => \\__pi_arg1 => (__pi_arg1)"
-    ]
-    6
-  ]
-
-test7 = "(:interpret \":cd C:/Path/to/dir\")"
-list7 =
-  [
-    ":interpret"
-    ":cd C:/Path/to/dir"
-  ]
-
-describe "The sub-parser(s)", ->
-  it "for :True and :False should work.", ->
-    expect(runP(parse.trueP, ':True')).toEqual(true)
-    expect(runP(parse.falseP, ':False')).toEqual(false)
-
-  it "for integers should work.", ->
-    expect(runP(parse.integerP, '2345')).toEqual(2345)
-    expect(runP(parse.integerP, '1')).toEqual(1)
-
-  it "for symbols should work.", ->
-    expect(runP(parse.symbolP, ':sym')).toEqual(':sym')
-
-  it "for string chars should work.", ->
-    expect(runP(parse.stringCharP, 'h')).toEqual('h')
-    expect(runP(parse.stringCharP, '\\"')).toEqual('"')
-
-  it "for strings should work.", ->
-    expect(runP(parse.stringP, '"hello"')).toEqual('hello')
-    expect(runP(parse.stringP, '"\\"Z\\""')).toEqual('"Z"')
-    expect(runP(parse.stringP, '"\\"Z\\" : String"')).toEqual('"Z" : String')
-
-describe "A parser", ->
-  it "should parse to the right list.", ->
-    expect(parse.parse(test1)).toEqual(list1)
-    expect(parse.parse(test2)).toEqual(list2)
-    expect(parse.parse(test3)).toEqual(list3)
-    expect(parse.parse(test4)).toEqual(list4)
-    expect(parse.parse(test5)).toEqual(list5)
-    expect(parse.parse(test6)).toEqual(list6)
-
-  it "should serialize back again.", ->
-    expect(sexpFormatter.formatSexp(list1)).toEqual(test1)
-    expect(sexpFormatter.formatSexp(list2)).toEqual(test2)
-    expect(sexpFormatter.formatSexp(list3)).toEqual(test3)
-    expect(sexpFormatter.formatSexp(list4)).toEqual(test4)
-    expect(sexpFormatter.formatSexp(list7)).toEqual(test7)
-
-  it "should serialize common commands.", ->
-    loadFile = [[':load-file', "idris.idr"], 1]
-    expect(sexpFormatter.formatSexp(loadFile)).toEqual '((:load-file "idris.idr") 1)'