Fixes #109

Author: swr1bm86

README.md

@@ -67,10 +67,11 @@ The following Visual Studio Code settings along with their *default* values that
 
 ```javascript
 {
-    "idris.executablePath": "idris", // The full path to the idris executable.
-    "idris.hoverMode": "fallback",   // Controls the hover behavior. 'info' will display Idris documentation, 'type' will display Idris type, 'fallback' will try 'info' first and fallback to 'type' if we can not get the documentation, and 'none' will disable hover tooltips.
-    "idris.suggestMode": "allWords"  // Controls the auto-completion behavior. 'allWords' will always include all words from the currently opened documentation, 'replCompletion' will get suggestions from Idris REPL process.
-    "idris.warnPartial": true        // Show warning when a function is partial.
+    "idris.executablePath": "idris",          // The full path to the idris executable.
+    "idris.hoverMode": "fallback",            // Controls the hover behavior. 'info' will display Idris documentation, 'type' will display Idris type, 'fallback' will try 'info' first and fallback to 'type' if we can not get the documentation, and 'none' will disable hover tooltips.
+    "idris.suggestMode": "allWords"           // Controls the auto-completion behavior. 'allWords' will always include all words from the currently opened documentation, 'replCompletion' will get suggestions from Idris REPL process.
+    "idris.warnPartial": false                // Show warning when a function is partial.
+    "idris.showOutputWhenTypechecking": false //Show output channel when typechecking finished."
 }
 ```
 

package.json

@@ -98,7 +98,7 @@
         },
         "idris.warnPartial": {
           "type": "boolean",
-          "default": true,
+          "default": false,
           "description": "Show warning when a function is partial."
         },
         "idris.hoverMode": {
@@ -120,6 +120,11 @@
           ],
           "default": "allWords",
           "description": "Controls the auto-completion behavior. 'allWords' will always include all words from the currently opened documentation, 'replCompletion' will get suggestions from Idris REPL process."
+        },
+        "idris.showOutputWhenTypechecking": {
+          "type": "boolean",
+          "default": false,
+          "description": "Show output channel when typechecking finished."
         }
       }
     },

src/idris/commands.js

@@ -209,10 +209,13 @@ let buildIPKG = (uri) => {
 }
 
 let typecheckFile = (uri) => {
+  let needShowOC = vscode.workspace.getConfiguration('idris').get('showOutputWhenTypechecking')
   let successHandler = (_) => {
-    outputChannel.clear()
-    outputChannel.show()
-    outputChannel.append("Idris: File loaded successfully")
+    if (needShowOC) {
+      outputChannel.clear()
+      outputChannel.show()
+      outputChannel.append("Idris: File loaded successfully")
+    }
     tcDiagnosticCollection.clear()
     typeCheckingStatusItem.text = "Idris: Type checking ✔︎"
     typeCheckingStatusItem.show()
@@ -224,9 +227,13 @@ let typecheckFile = (uri) => {
       return arg.responseType === 'return'
     }).subscribe(successHandler, (err) => {
       destroy(true)
-      displayErrors(err)
+      if (needShowOC) {
+        displayErrors(err)
+      }
     })
-    showLoading()
+    if (needShowOC) {
+      showLoading()
+    }
     resolve()
   }).then(function () {
   }).catch(function () {