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;
--- 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",