Fixes #88

package.json

@@ -367,6 +367,11 @@
         "command": "idris.new-project",
         "title": "Idris: New Project",
         "description": "Create a new ipkg based project using idringen"
+      },
+      {
+        "command": "idris.search",
+        "title": "Idris: Search for values by type",
+        "description": "Search Idris values by a concrete type signature"
       }
     ],
     "snippets": [

src/controller.js

@@ -32,7 +32,8 @@ let getCommands = () => {
     ['idris.start-refresh-repl', runCommand(commands.startREPL)],
     ['idris.send-selection-repl', runCommand(commands.sendREPL)],
     ['idris.cleanup-ibc', runCommand(cleanupIbc)],
-    ['idris.new-project', newProject]
+    ['idris.new-project', newProject],
+    ['idris.search', runCommand(commands.search)]
   ]
 }
 

src/idris/commands.js

@@ -346,12 +346,18 @@ let evalSelection = (uri) => {
   })
 }
 
-let startup = (uri) => {
+let createIdrisTerm = () => {
   const pathToIdris = vscode.workspace.getConfiguration('idris').get('executablePath');
   const idrisPath = which.sync(pathToIdris)
   const pkgOpts = ipkg.getPkgOpts(innerCompilerOptions)
   term = vscode.window.createTerminal("Idris REPL", idrisPath, pkgOpts)
 
+  return term
+}
+
+let startup = (uri) => {
+  let term = createIdrisTerm()
+
   if (innerCompilerOptions.src && uri.includes(innerCompilerOptions.src)) {
     term.sendText(`:cd ${path.resolve(innerCompilerOptions.src)}`.replace(/\\/g, "/"))
     uri = path.relative(path.resolve(innerCompilerOptions.src), path.resolve(uri))
@@ -361,16 +367,32 @@ let startup = (uri) => {
   term.show()
 }
 
-let startREPL = (uri) => {
+let toggleTerm = (action, arg) => {
   if (term == null) {
-    startup(uri)
+    action(arg)
   } else {
     term.hide()
     term.dispose()
-    startup(uri)
+    action(arg)
   }
 }
 
+let search = (_) => {
+  vscode.window.showInputBox({ prompt: 'Type signature' }).then(sig => {
+    let searchInTerm = (sig) => {
+      let term = createIdrisTerm()
+
+      term.sendText(`:search ${sig}`)
+      term.show()
+    }
+    toggleTerm(searchInTerm, sig)
+  })
+}
+
+let startREPL = (uri) => {
+  toggleTerm(startup, uri)
+}
+
 let sendREPL = (uri) => {
   let editor = vscode.window.activeTextEditor
   let selection = editor.selection
@@ -716,5 +738,6 @@ module.exports = {
   clearOutputChannel,
   buildIPKG,
   checkTotality,
-  clearTotalityDiagnostics
+  clearTotalityDiagnostics,
+  search
 }

src/idris/model.js

@@ -8,9 +8,11 @@ class IdrisModel {
     this.requestId = 0
     this.ideModeRef = null
     this.idrisBuildRef = null
+    this.idrisReplRef = null
     this.subjects = {}
     this.warnings = {}
     this.idrisBuildSubject = null
+    this.idrisReplSubject = null
     this.compilerOptions = {}
   }
 
@@ -27,7 +29,7 @@ class IdrisModel {
 
   idrisBuild(compilerOptions, ipkgFile) {
     this.idrisBuildRef = new IdrisBuild(ipkgFile)
-    this.idrisBuildRef.on('message', (obj) => { this.handleIdrisBuildCommand(obj) })
+    this.idrisBuildRef.on('message', (obj) => { this.handleIdrisBuildMessage(obj) })
     this.idrisBuildRef.start(compilerOptions)
     return this.idrisBuildRef
   }
@@ -39,6 +41,8 @@ class IdrisModel {
   stop() {
     if (this.ideModeRef)
       this.ideModeRef.stop()
+    if (this.idrisReplRef)
+      this.idrisReplRef.stop()
   }
 
   setCompilerOptions(options) {
@@ -58,8 +62,8 @@ class IdrisModel {
     return ++this.requestId
   }
 
-  handleIdrisBuildCommand(cmd) {
-    this.idrisBuildSubject.onNext(cmd)
+  handleIdrisBuildMessage(msg) {
+    this.idrisBuildSubject.onNext(msg)
   }
 
   handleIdeModeCommand(cmd) {