# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1721336569 -7200
# Node ID 132080f5d15cabc455e7dd0a37a8ad6bff6a228f
# Parent  6aafcdc0217f1ccd04f29d524e576760dcffa4e3
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;

diff -r 6aafcdc0217f -r 132080f5d15c src/Tools/VSCode/extension/isabelle-language.json
--- 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": ".+"
 }
diff -r 6aafcdc0217f -r 132080f5d15c src/Tools/VSCode/src/vscode_main.scala
--- 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",