Fixes #76

Author: swr1bm86

package.json

@@ -143,50 +143,55 @@
           "group": "idris@5"
         },
         {
-          "command": "idris.case-split",
+          "command": "idris.add-proof-clause",
           "when": "editorFocus && editorLangId == idris",
           "group": "idris@6"
         },
         {
-          "command": "idris.proof-search",
+          "command": "idris.case-split",
           "when": "editorFocus && editorLangId == idris",
           "group": "idris@7"
         },
         {
-          "command": "idris.make-with",
+          "command": "idris.proof-search",
           "when": "editorFocus && editorLangId == idris",
           "group": "idris@8"
         },
         {
-          "command": "idris.make-case",
+          "command": "idris.make-with",
           "when": "editorFocus && editorLangId == idris",
           "group": "idris@9"
         },
         {
-          "command": "idris.make-lemma",
+          "command": "idris.make-case",
           "when": "editorFocus && editorLangId == idris",
           "group": "idris@10"
         },
         {
-          "command": "idris.eval-selection",
+          "command": "idris.make-lemma",
           "when": "editorFocus && editorLangId == idris",
           "group": "idris@11"
         },
         {
-          "command": "idris.start-refresh-repl",
+          "command": "idris.eval-selection",
           "when": "editorFocus && editorLangId == idris",
           "group": "idris@12"
         },
         {
-          "command": "idris.send-selection-repl",
+          "command": "idris.start-refresh-repl",
           "when": "editorFocus && editorLangId == idris",
           "group": "idris@13"
         },
         {
-          "command": "idris.cleanup-ibc",
+          "command": "idris.send-selection-repl",
           "when": "editorFocus && editorLangId == idris",
           "group": "idris@14"
         },
+        {
+          "command": "idris.cleanup-ibc",
+          "when": "editorFocus && editorLangId == idris",
+          "group": "idris@15"
+        },
         {
           "command": "idris.typecheck",
           "when": "editorFocus && editorLangId == lidris",
@@ -213,49 +218,54 @@
           "group": "idris@5"
         },
         {
-          "command": "idris.case-split",
+          "command": "idris.add-proof-clause",
           "when": "editorFocus && editorLangId == lidris",
           "group": "idris@6"
         },
         {
-          "command": "idris.proof-search",
+          "command": "idris.case-split",
           "when": "editorFocus && editorLangId == lidris",
           "group": "idris@7"
         },
         {
-          "command": "idris.make-with",
+          "command": "idris.proof-search",
           "when": "editorFocus && editorLangId == lidris",
           "group": "idris@8"
         },
         {
-          "command": "idris.make-case",
+          "command": "idris.make-with",
           "when": "editorFocus && editorLangId == lidris",
           "group": "idris@9"
         },
         {
-          "command": "idris.make-lemma",
+          "command": "idris.make-case",
           "when": "editorFocus && editorLangId == lidris",
           "group": "idris@10"
         },
         {
-          "command": "idris.eval-selection",
+          "command": "idris.make-lemma",
           "when": "editorFocus && editorLangId == lidris",
           "group": "idris@11"
         },
         {
-          "command": "idris.start-refresh-repl",
+          "command": "idris.eval-selection",
           "when": "editorFocus && editorLangId == lidris",
           "group": "idris@12"
         },
         {
-          "command": "idris.send-selection-repl",
+          "command": "idris.start-refresh-repl",
           "when": "editorFocus && editorLangId == lidris",
           "group": "idris@13"
         },
         {
-          "command": "idris.cleanup-ibc",
+          "command": "idris.send-selection-repl",
           "when": "editorFocus && editorLangId == lidris",
           "group": "idris@14"
+        },
+        {
+          "command": "idris.cleanup-ibc",
+          "when": "editorFocus && editorLangId == lidris",
+          "group": "idris@15"
         }
       ]
     },
@@ -290,6 +300,11 @@
         "title": "Idris: Generate an initial pattern match clause",
         "description": "Add an initial pattern match clause"
       },
+      {
+        "command": "idris.add-proof-clause",
+        "title": "Idris: Generate an initial pattern match clause when trying to proof a type",
+        "description": "http://docs.idris-lang.org/en/latest/reference/misc.html#match-application"
+      },
       {
         "command": "idris.case-split",
         "title": "Idris: Generate a case split for the pattern variable",

src/controller.js

@@ -17,6 +17,7 @@ let getCommands = () => {
     ['idris.print-definition', runCommand(commands.printDefinition)],
     ['idris.show-holes', runCommand(commands.showHoles)],
     ['idris.add-clause', runCommand(commands.addClause)],
+    ['idris.add-proof-clause', runCommand(commands.addProofClause)],
     ['idris.case-split', runCommand(commands.caseSplit)],
     ['idris.proof-search', runCommand(commands.proofSearch)],
     ['idris.make-with', runCommand(commands.makeWith)],

src/idris/commands.js

@@ -416,6 +416,35 @@ let addClause = (uri) => {
   })
 }
 
+let addProofClause = (uri) => {
+  let currentWord = getWord()
+  if (!currentWord) return
+  let editor = vscode.window.activeTextEditor
+  let line = editor.selection.active.line
+
+  let successHandler = (arg) => {
+    let clause = arg.msg[0] + "\n"
+    editor.edit((edit) => {
+      edit.insert(new vscode.Position(line + 1, 0), line + 1 == editor.document.lineCount ? "\n" + clause : clause)
+    })
+
+    outputChannel.clear()
+    needDestroy = true
+  }
+
+  new Promise((resolve, reject) => {
+    model.load(uri).filter((arg) => {
+      return arg.responseType === 'return'
+    }).flatMap(() => {
+      return model.addProofClause(line + 1, currentWord)
+    }).subscribe(handlerWrapper(successHandler), displayErrors)
+    showLoading()
+    resolve()
+  }).then(function () {
+  }).catch(function () {
+  })
+}
+
 let caseSplit = (uri) => {
   let currentWord = getWord()
   if (!currentWord) return
@@ -674,6 +703,7 @@ module.exports = {
   printDefinition,
   showHoles,
   addClause,
+  addProofClause,
   caseSplit,
   proofSearch,
   makeWith,

src/idris/model.js

@@ -181,6 +181,10 @@ class IdrisModel {
     return this.prepareCommand([':add-clause', line, word])
   }
 
+  addProofClause(line, word) {
+    return this.prepareCommand([':add-proof-clause', line, word])
+  }
+
   caseSplit(line, word) {
     return this.prepareCommand([':case-split', line, word])
   }