Fix #30 and Fix #31

anoma · Jan 19, 2023 · 623933c · 623933c
1 parent 353d116
commit 623933c
Show file tree

Hide file tree

Showing 5 changed files with 64 additions and 66 deletions.
diff --git a/language-configuration.json b/language-configuration.json
@@ -1,23 +1,18 @@
 {
   "comments": {
-    // symbol used for single line comment. Remove this entry if your language does not support line comments
-    // "lineComment": "--",
-    // // symbols used for start and end a block comment. Remove this entry if your language does not support block comments
-    // "blockComment": ["{-", "-}"]
-  },
-  // symbols used as brackets
+    "blockComment": ["{-", "-}"],
+    "lineComment": "--"
+  }, // symbols used as brackets
   "brackets": [
     ["{", "}"],
-    ["[", "]"],
     ["(", ")"]
   ],
   // symbols that are auto closed when typing
   "autoClosingPairs": [
     ["{", "}"],
     ["[", "]"],
     ["(", ")"],
-    ["\"", "\""],
-    ["'", "'"]
+    ["\"", "\""]
   ],
   // symbols that can be used to surround a selection
   "surroundingPairs": [

diff --git a/package.json b/package.json
@@ -1,10 +1,10 @@
 {
   "name": "juvix-mode",
-  "version": "0.1.20",
+  "version": "0.1.21",
   "license": "GPL-3.0",
   "description": "Juvix Mode for VSCode",
   "displayName": "Juvix",
-  "publisher": "heliax",
+  "publisher": "Heliax",
   "icon": "assets/tara.png",
   "repository": {
     "type": "git",
@@ -28,9 +28,6 @@
     "language",
     "programming"
   ],
-  "galleryBanner": {
-    "theme": "dark"
-  },
   "main": "./out/extension.js",
   "scripts": {
     "vscode:prepublish": "npm run package",
@@ -97,7 +94,7 @@
         "[*Light*]": {
           "rules": {
             "axiom": {
-              "foreground": "#e70000"
+              "foreground": "#ad1313"
             },
             "comment": {
               "foreground": "#a8a8a8",
@@ -463,7 +460,7 @@
         },
         "juvix-mode.typecheckOn": {
           "type": "string",
-          "default": "save",
+          "default": "none",
           "enum": [
             "change",
             "save",
@@ -478,8 +475,16 @@
         "juvix-mode.opts": {
           "type": "object",
           "order": 1,
-          "description": "Global flags for the Juvix CLI.",
+          "description": "Common options for the Juvix CLI.",
           "properties": {
+            "internalBuildDir": {
+              "type": "string",
+              "description": "Directory for compiler internal output. Empty string will make the compiler use a temporary directory."
+            },
+            "judocDir": {
+              "type": "string",
+              "description": "Directory for html output. Empty string will make the compiler use a temporary directory."
+            },
             "noColors": {
               "type": "boolean",
               "description": "Disable ANSI formatting"
@@ -503,20 +508,12 @@
             "noStdlib": {
               "type": "boolean",
               "description": "Do not use the standard library"
-            },
-            "internalBuildDir": {
-              "type": "string",
-              "default": ".juvix-build",
-              "description": "Directory for compiler internal output. Empty string will make the compiler use a temporary directory."
-            },
-            "judocDir": {
-              "type": "string",
-              "default": "html",
-              "description": "Directory for html output. Empty string will make the compiler use a temporary directory."
             }
           },
           "additionalProperties": false,
           "default": {
+            "internalBuildDir": ".juvix-build",
+            "judocDir": "html",
             "noColors": false,
             "showNameIds": false,
             "onlyErrors": false,

diff --git a/snippets/Debug.code-snippets b/snippets/Debug.code-snippets
@@ -1,98 +1,98 @@
 {
   "All": {
     "prefix": ["debug-all"],
-    "body": "$BLOCK_COMMENT_START DEBUG: All $BLOCK_COMMENT_END"
+    "body": "DEBUG: All"
   },
   "None": {
     "prefix": ["debug-none"],
-    "body": "$BLOCK_COMMENT_START NO-DEBUG! $BLOCK_COMMENT_END"
+    "body": "NO-DEBUG!"
   },
   "Parsed": {
     "prefix": ["debug-parse"],
-    "body": "$BLOCK_COMMENT_START DEBUG: sed $BLOCK_COMMENT_END"
+    "body": "DEBUG: sed"
   },
   "Scoped": {
     "prefix": ["debug-scope"],
-    "body": "$BLOCK_COMMENT_START DEBUG: Scoped"
+    "body": "DEBUG: Scoped"
   },
   "HighlightJSON": {
     "prefix": ["debug-highlight-json"],
-    "body": "$BLOCK_COMMENT_START DEBUG: HighlightJSON $BLOCK_COMMENT_END"
+    "body": "DEBUG: HighlightJSON"
   },
   "Highlight": {
     "prefix": ["debug-highlight"],
-    "body": "$BLOCK_COMMENT_START DEBUG: Highlight $BLOCK_COMMENT_END"
+    "body": "DEBUG: Highlight"
   },
   "InternalPretty": {
     "prefix": ["debug-internal-pretty"],
-    "body": "$BLOCK_COMMENT_START DEBUG: ernalPretty $BLOCK_COMMENT_END"
+    "body": "DEBUG: InternalPretty"
   },
   "InternalArity": {
     "prefix": ["debug-internal-arity"],
-    "body": "$BLOCK_COMMENT_START DEBUG: InternalArity $BLOCK_COMMENT_END"
+    "body": "DEBUG: InternalArity"
   },
   "InternalTypecheck": {
     "prefix": ["debug-internal-typecheck"],
-    "body": "$BLOCK_COMMENT_START DEBUG: InternalTypecheck $BLOCK_COMMENT_END"
+    "body": "DEBUG: InternalTypecheck"
   },
   "InternalCoreEval": {
     "prefix": ["debug-internal-core-eval"],
-    "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEval $BLOCK_COMMENT_END"
+    "body": "DEBUG: InternalCoreEval"
   },
   "InternalCoreEvalShowDeBruijn": {
     "prefix": ["debug-internal-core-eval-show-de-bruijn"],
-    "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEvalShowDeBruijn $BLOCK_COMMENT_END"
+    "body": "DEBUG: InternalCoreEvalShowDeBruijn"
   },
   "InternalCoreEvalTransformsLifting": {
     "prefix": ["debug-lifting"],
-    "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEvalTransformsLifting $BLOCK_COMMENT_END"
+    "body": "DEBUG: InternalCoreEvalTransformsLifting"
   },
   "InternalCoreEvalTransformsMoveApps": {
     "prefix": ["debug-move-apps"],
-    "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEvalTransformsMoveApps $BLOCK_COMMENT_END"
+    "body": "DEBUG: InternalCoreEvalTransformsMoveApps"
   },
   "InternalCoreEvalTransformsRemoveTypeArgs": {
     "prefix": ["debug-remove-type-args"],
-    "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEvalTransformsRemoveTypeArgs $BLOCK_COMMENT_END"
+    "body": "DEBUG: InternalCoreEvalTransformsRemoveTypeArgs"
   },
   "InternalCoreEvalTransformsRemoveTopEtaExpand": {
     "prefix": ["debug-remove-top-eta-expand"],
-    "body": "$BLOCK_COMMENT_START DEBUG: ernalCoreEvalTransformsRemoveTopEtaExpand $BLOCK_COMMENT_END"
+    "body": "DEBUG: InternalCoreEvalTransformsRemoveTopEtaExpand"
   },
   "CoreEval": {
     "prefix": ["debug-core-eval"],
-    "body": "$BLOCK_COMMENT_START DEBUG: CoreEval $BLOCK_COMMENT_END"
+    "body": "DEBUG: CoreEval"
   },
   "CoreRead": {
     "prefix": ["debug-core-read"],
-    "body": "$BLOCK_COMMENT_START DEBUG: CoreRead $BLOCK_COMMENT_END"
+    "body": "DEBUG: CoreRead"
   },
   "AsmRun": {
     "prefix": ["debug-asm-run"],
-    "body": "$BLOCK_COMMENT_START DEBUG: AsmRun $BLOCK_COMMENT_END"
+    "body": "DEBUG: AsmRun"
   },
   "AsmValidate": {
     "prefix": ["debug-asm-validate"],
-    "body": "$BLOCK_COMMENT_START DEBUG: AsmValidate $BLOCK_COMMENT_END"
+    "body": "DEBUG: AsmValidate"
   },
   "AsmCompile": {
     "prefix": ["debug-asm-compile"],
-    "body": "$BLOCK_COMMENT_START DEBUG: AsmCompile $BLOCK_COMMENT_END"
+    "body": "DEBUG: AsmCompile"
   },
   "RuntimeCompile": {
     "prefix": ["debug-runtime-compile"],
-    "body": "$BLOCK_COMMENT_START DEBUG: RuntimeCompile $BLOCK_COMMENT_END"
+    "body": "DEBUG: RuntimeCompile"
   },
   "Root": {
     "prefix": ["debug-root"],
-    "body": "$BLOCK_COMMENT_START DEBUG: Root $BLOCK_COMMENT_END"
+    "body": "DEBUG: Root"
   },
   "TerminationCalls": {
     "prefix": ["debug-termination-calls"],
-    "body": "$BLOCK_COMMENT_START DEBUG: TerminationCalls $BLOCK_COMMENT_END"
+    "body": "DEBUG: TerminationCalls"
   },
   "TerminationGraph": {
     "prefix": ["debug-termination-graph"],
-    "body": "$BLOCK_COMMENT_START DEBUG: TerminationGraph"
+    "body": "DEBUG: TerminationGraph"
   }
 }
diff --git a/src/config.ts b/src/config.ts
@@ -10,6 +10,8 @@ import * as path from 'path';
 import { tmpdir } from 'os';
 import { debugChannel } from './utils/debug';
 
+let juvixBuildDir: string | undefined;
+
 export class JuvixConfig {
   readonly binaryName = new VsCodeSetting('juvix-mode.bin.name', {
     serializer: serializerWithDefault('Juvix'),
@@ -39,17 +41,22 @@ export class JuvixConfig {
 
   readonly judocDir = new VsCodeSetting('juvix-mode.opts.judocDir');
 
-  public getInternalBuildDir(): string {
+  public getInternalBuildDir(): string | undefined {
+    if (juvixBuildDir) return juvixBuildDir;
     const buildDir = this.internalBuildDir.get();
-    if (buildDir) return buildDir.toString();
-    const tmp = path.join(tmpdir(), fs.mkdtempSync('juvix'));
+    if (buildDir) {
+      juvixBuildDir = buildDir.toString();
+      return juvixBuildDir;
+    }
+    const tmp = path.join(tmpdir(), fs.mkdtempSync('.juvix-build'));
     try {
       fs.mkdirSync(tmp);
-      return tmp.toString();
+      juvixBuildDir = tmp.toString();
+      return juvixBuildDir;
     } catch (e) {
       debugChannel.error('Error creating temporary directory: ' + e);
     }
-    return '.juvix-build';
+    return juvixBuildDir;
   }
 
   public getJudocdDir(): string {
@@ -89,8 +96,11 @@ export class JuvixConfig {
     if (this.noTermination.get()) flags.push('--no-termination');
     if (this.noPositivity.get()) flags.push('--no-positivity');
     if (this.noStdlib.get()) flags.push('--no-stdlib');
-    flags.push('--internal-build-dir');
-    flags.push(this.getInternalBuildDir());
+    const buildDir = this.getInternalBuildDir();
+    if (buildDir) {
+      flags.push('--internal-build-dir');
+      flags.push(buildDir);
+    }
     return flags.join(' ').trim();
   }
 

diff --git a/src/tasks.ts b/src/tasks.ts
@@ -4,7 +4,6 @@
 
 import * as vscode from 'vscode';
 import * as user from './config';
-import { isJuvixFile } from './utils/base';
 import { debugChannel } from './utils/debug';
 
 export const TASK_TYPE = 'Juvix';
@@ -27,14 +26,11 @@ export async function activate(context: vscode.ExtensionContext) {
   }
 
   const provider = new JuvixTaskProvider();
-  const juvixTasks = provider.provideTasks();
-  const taskProvider: vscode.Disposable = vscode.tasks.registerTaskProvider(
-    TASK_TYPE,
-    provider
+  const juvixTasks: Promise<vscode.Task[]> = provider.provideTasks();
+  context.subscriptions.push(
+    vscode.tasks.registerTaskProvider(TASK_TYPE, provider)
   );
-  context.subscriptions.push(taskProvider);
 
-  const config = new user.JuvixConfig();
   juvixTasks
     .then(tasks => {
       for (const task of tasks) {
@@ -96,7 +92,7 @@ export class JuvixTaskProvider implements vscode.TaskProvider {
         command: 'typecheck',
         args: ['${file}'],
         group: vscode.TaskGroup.Build,
-        reveal: vscode.TaskRevealKind.Silent,
+        reveal: vscode.TaskRevealKind.Always,
       },
       {
         command: 'compile',