vscode: further adjusted default settings and wordPattern for consistent completion popups;
authorThomas Lindae <thomas.lindae@in.tum.de>
Thu, 18 Jul 2024 23:02:49 +0200
changeset 81082 132080f5d15c
parent 81081 6aafcdc0217f
child 81083 aa77be3e8329
vscode: further adjusted default settings and wordPattern for consistent completion popups; for some reason wordPattern must be set to match (almost) everything, otherwise completions only pop up every other character, and then we must disable wordBasedSuggestions or it will suggest whole lines out of the document;
src/Tools/VSCode/extension/isabelle-language.json
src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/extension/isabelle-language.json	Thu Jul 18 17:59:50 2024 +0200
+++ b/src/Tools/VSCode/extension/isabelle-language.json	Thu Jul 18 23:02:49 2024 +0200
@@ -44,5 +44,6 @@
     ["⦃", "⦄"],
     ["`", "`"],
     ["\"", "\""]
-  ]
+  ],
+  "wordPattern": ".+"
 }
--- a/src/Tools/VSCode/src/vscode_main.scala	Thu Jul 18 17:59:50 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_main.scala	Thu Jul 18 23:02:49 2024 +0200
@@ -150,6 +150,7 @@
     "editor.rulers": [80, 100],
     "editor.quickSuggestions": { "strings": "on" },
     "editor.unicodeHighlight.ambiguousCharacters": false,
+    "editor.wordBasedSuggestions": false,
     "extensions.autoCheckUpdates": false,
     "extensions.autoUpdate": false,
     "terminal.integrated.fontFamily": "monospace",