# HG changeset patch
# User wenzelm
# Date 1645562069 -3600
# Node ID 79fab5ff41639e6eeb6654a41f20b4a67c4c72e5
# Parent  18cd39e55eca17e924067f47128a67d239825a63# Parent  122d1d1a16fd7684b8f8a63e78b2cd5424154942
merged

diff -r 18cd39e55eca -r 79fab5ff4163 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Feb 22 15:00:04 2022 +0100
+++ b/CONTRIBUTORS	Tue Feb 22 21:34:29 2022 +0100
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* April - August 2021: Denis Paluca and Fabian Huch, TU München
+  Various improvements to Isabelle/VSCode.
+
 
 Contributions to Isabelle2021-1
 -------------------------------
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/README.md
--- a/src/Tools/VSCode/extension/README.md	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/README.md	Tue Feb 22 21:34:29 2022 +0100
@@ -75,72 +75,13 @@
       + *bibtexLanguage* (optional): it gives `.bib` a formal status, thus
         `@{cite}` antiquotations become active for completion and hyperlinks.
 
-  * Open the dialog *Preferences / User settings* and provide the following
-    entries in the second window, where local user additions are stored:
-
-      + On all platforms: `isabelle.home` needs to point to the main Isabelle
-      directory (`$ISABELLE_HOME`).
-
-      + On Windows: use drive-letter and backslashes for `isabelle.home` above.
-      When running from a bare repository clone (not a development snapshot),
-      `isabelle.cygwin_home` needs to point to a suitable Cygwin installation.
-
-    Examples:
-
-      + Linux:
-        ```
-        "isabelle.home": "/home/makarius/Isabelle"
-        ```
-
-      + Mac OS X:
-        ```
-        "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
-        ```
-
-      + Windows:
-        ```
-        "isabelle.home": "C:\\Users\\makarius\\Isabelle"
-        ```
-
   * Restart the VSCode application to ensure that all extensions are properly
   initialized and user settings are updated. Afterwards VSCode should know about
   `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules).
 
   The Isabelle extension is initialized when the first Isabelle file is opened.
   It requires a few seconds to start up: a small popup window eventually says
-  *"Welcome to Isabelle ..."*. If that fails, there might be something wrong
-  with `isabelle.home` from above, or the Isabelle distribution does not fit to
-  the version of the VSCode extension from the Marketplace.
-
-
-### Support for Isabelle symbols
-
-Isabelle symbols like `\<forall>` are rendered using the extension *Prettify
-Symbols Mode*, which needs to be installed separately.
-
-In addition, the following user settings should be changed in the *Preferences /
-User settings* dialog of VSCode:
-
-```
-"prettifySymbolsMode.substitutions": [
-  {
-    "language": "isabelle",
-    "revealOn": "none",
-    "adjustCursorMovement": true,
-    "prettyCursor": "none",
-    "substitutions": []
-  },
-  {
-    "language": "isabelle-ml",
-    "revealOn": "none",
-    "adjustCursorMovement": true,
-    "prettyCursor": "none",
-    "substitutions": []
-  }]
-```
-
-Actual symbol replacement tables are provided by the prover process on startup,
-based on the usual `etc/symbols` specifications of the Isabelle installation.
+  *"Welcome to Isabelle ..."*.
 
 
 ### Further Preferences
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/media/main.js
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/main.js	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,27 @@
+(function () {
+    const vscode = acquireVsCodeApi();
+        
+    for (const link of document.querySelectorAll('a[href^="file:"]')) {
+        link.addEventListener('click', () => {
+            vscode.postMessage({
+                command: "open",
+                link: link.getAttribute('href'),
+            });
+        });
+    }
+    
+    const auto_update = document.getElementById('auto_update');
+    auto_update && auto_update.addEventListener('change', (e) => {
+            vscode.postMessage({'command': 'auto_update', 'enabled': e.target.checked}) ;
+        });
+
+    const update_button = document.getElementById('update_button');
+    update_button && update_button.addEventListener('click', (e) => {
+            vscode.postMessage({'command': 'update'}) 
+        });
+        
+    const locate_button = document.getElementById('locate_button');
+    locate_button && locate_button.addEventListener('click', (e) => {
+            vscode.postMessage({'command': 'locate'});
+        });
+}());
\ No newline at end of file
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/media/vscode.css
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/vscode.css	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,113 @@
+:root {
+  --container-paddding: 20px;
+  --input-padding-vertical: 6px;
+  --input-padding-horizontal: 4px;
+  --input-margin-vertical: 4px;
+  --input-margin-horizontal: 0;
+}
+
+body {
+  padding: 0 var(--container-paddding);
+  color: var(--vscode-foreground);
+  font-size: var(--vscode-font-size);
+  font-weight: var(--vscode-font-weight);
+  font-family: var(--vscode-font-family);
+  background-color: var(--vscode-editor-background);
+}
+
+ol,
+ul {
+  padding-left: var(--container-paddding);
+}
+
+body > *,
+form > * {
+  margin-block-start: var(--input-margin-vertical);
+  margin-block-end: var(--input-margin-vertical);
+}
+
+*:focus {
+  outline-color: var(--vscode-focusBorder) !important;
+}
+
+a {
+  color: var(--vscode-textLink-foreground);
+  text-decoration: none;
+}
+
+a:hover,
+a:active {
+  color: var(--vscode-textLink-activeForeground);
+}
+
+code {
+  font-size: var(--vscode-editor-font-size);
+  font-family: var(--vscode-editor-font-family);
+}
+
+button {
+  border: none;
+  padding: var(--input-padding-vertical) var(--input-padding-horizontal);
+  width: 20%;
+  text-align: center;
+  outline: 1px solid transparent;
+  outline-offset: 2px !important;
+  color: var(--vscode-button-foreground);
+  background: var(--vscode-button-background);
+}
+
+button:hover {
+  cursor: pointer;
+  background: var(--vscode-button-hoverBackground);
+}
+
+button:focus {
+  outline-color: var(--vscode-focusBorder);
+}
+
+button.secondary {
+  color: var(--vscode-button-secondaryForeground);
+  background: var(--vscode-button-secondaryBackground);
+}
+
+button.secondary:hover {
+  background: var(--vscode-button-secondaryHoverBackground);
+}
+
+input:not([type='checkbox']),
+textarea {
+  display: block;
+  width: 100%;
+  border: none;
+  font-family: var(--vscode-font-family);
+  padding: var(--input-padding-vertical) var(--input-padding-horizontal);
+  color: var(--vscode-input-foreground);
+  outline-color: var(--vscode-input-border);
+  background-color: var(--vscode-input-background);
+}
+
+input::placeholder,
+textarea::placeholder {
+  color: var(--vscode-input-placeholderForeground);
+}
+
+#controls {
+  display: flex;
+  flex-direction: row;
+  justify-content: flex-end;
+  align-items: center;
+}
+
+#controls > *{
+  margin-left: 5px;
+  margin-top: 5px;
+}
+
+/* line break for pre  */
+pre {
+  white-space: pre-wrap;     /* Since CSS 2.1 */
+  white-space: -moz-pre-wrap;/* Mozilla, since 1999 */
+  white-space: -pre-wrap;    /* Opera 4-6 */
+  white-space: -o-pre-wrap;  /* Opera 7 */
+  word-wrap: break-word;     /* Internet Explorer 5.5+ */
+}
\ No newline at end of file
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/package.json	Tue Feb 22 21:34:29 2022 +0100
@@ -174,11 +174,6 @@
         "configuration": {
             "title": "Isabelle",
             "properties": {
-                "isabelle.home": {
-                    "type": "string",
-                    "default": "",
-                    "description": "Main Isabelle directory (ISABELLE_HOME)."
-                },
                 "isabelle.args": {
                     "type": "array",
                     "items": {
@@ -187,369 +182,133 @@
                     "default": [],
                     "description": "Command-line arguments for isabelle vscode_server process."
                 },
-                "isabelle.cygwin_root": {
-                    "type": "string",
-                    "default": "",
-                    "description": "Cygwin installation on Windows (only relevant when running directly from the Isabelle repository)."
-                },
-                "isabelle.unprocessed_light_color": {
-                    "type": "string",
-                    "default": "rgba(255, 160, 160, 1.00)"
-                },
-                "isabelle.unprocessed_dark_color": {
-                    "type": "string",
-                    "default": "rgba(97, 0, 97, 1.00)"
-                },
-                "isabelle.unprocessed1_light_color": {
-                    "type": "string",
-                    "default": "rgba(255, 160, 160, 0.20)"
-                },
-                "isabelle.unprocessed1_dark_color": {
-                    "type": "string",
-                    "default": "rgba(97, 0, 97, 0.20)"
-                },
-                "isabelle.running_light_color": {
-                    "type": "string",
-                    "default": "rgba(97, 0, 97, 1.00)"
-                },
-                "isabelle.running_dark_color": {
-                    "type": "string",
-                    "default": "rgba(255, 160, 160, 1.00)"
-                },
-                "isabelle.running1_light_color": {
-                    "type": "string",
-                    "default": "rgba(97, 0, 97, 0.40)"
-                },
-                "isabelle.running1_dark_color": {
-                    "type": "string",
-                    "default": "rgba(255, 160, 160, 0.40)"
-                },
-                "isabelle.canceled_light_color": {
+                "isabelle.replacement": {
                     "type": "string",
-                    "default": "rgba(255, 106, 106, 0.40)"
-                },
-                "isabelle.canceled_dark_color": {
-                    "type": "string",
-                    "default": "rgba(255, 106, 106, 0.40)"
-                },
-                "isabelle.bad_light_color": {
-                    "type": "string",
-                    "default": "rgba(255, 106, 106, 0.40)"
-                },
-                "isabelle.bad_dark_color": {
-                    "type": "string",
-                    "default": "rgba(255, 106, 106, 0.40)"
-                },
-                "isabelle.intensify_light_color": {
-                    "type": "string",
-                    "default": "rgba(255, 204, 102, 0.40)"
-                },
-                "isabelle.intensify_dark_color": {
-                    "type": "string",
-                    "default": "rgba(204, 136, 0, 0.20)"
-                },
-                "isabelle.markdown_bullet1_light_color": {
-                    "type": "string",
-                    "default": "rgba(218, 254, 218, 1.00)"
-                },
-                "isabelle.markdown_bullet1_dark_color": {
-                    "type": "string",
-                    "default": "rgba(5, 199, 5, 0.20)"
-                },
-                "isabelle.markdown_bullet2_light_color": {
-                    "type": "string",
-                    "default": "rgba(255, 240, 204, 1.00)"
-                },
-                "isabelle.markdown_bullet2_dark_color": {
-                    "type": "string",
-                    "default": "rgba(204, 143, 0, 0.20)"
-                },
-                "isabelle.markdown_bullet3_light_color": {
-                    "type": "string",
-                    "default": "rgba(231, 231, 255, 1.00)"
-                },
-                "isabelle.markdown_bullet3_dark_color": {
-                    "type": "string",
-                    "default": "rgba(0, 0, 204, 0.20)"
+                    "default": "non-alphanumeric",
+                    "enum": [
+                        "none",
+                        "non-alphanumeric",
+                        "all"
+                    ],
+                    "enumDescriptions": [
+                        "Replacments are deactivated. No replacments are done.",
+                        "Replaces all uniqe abbreviations that contain no alphanumeric characters",
+                        "Replaces all uniqe abbreviations"
+                    ],
+                    "description": "Symbol replacement mode."
                 },
-                "isabelle.markdown_bullet4_light_color": {
-                    "type": "string",
-                    "default": "rgba(255, 224, 240, 1.00)"
-                },
-                "isabelle.markdown_bullet4_dark_color": {
-                    "type": "string",
-                    "default": "rgba(204, 0, 105, 0.20)"
-                },
-                "isabelle.quoted_light_color": {
-                    "type": "string",
-                    "default": "rgba(139, 139, 139, 0.10)"
-                },
-                "isabelle.quoted_dark_color": {
-                    "type": "string",
-                    "default": "rgba(150, 150, 150, 0.15)"
-                },
-                "isabelle.antiquoted_light_color": {
-                    "type": "string",
-                    "default": "rgba(255, 200, 50, 0.10)"
-                },
-                "isabelle.antiquoted_dark_color": {
-                    "type": "string",
-                    "default": "rgba(255, 214, 102, 0.15)"
-                },
-                "isabelle.writeln_light_color": {
-                    "type": "string",
-                    "default": "rgba(192, 192, 192, 1.0)"
-                },
-                "isabelle.writeln_dark_color": {
-                    "type": "string",
-                    "default": "rgba(192, 192, 192, 1.0)"
-                },
-                "isabelle.information_light_color": {
-                    "type": "string",
-                    "default": "rgba(193, 223, 238, 1.0)"
-                },
-                "isabelle.information_dark_color": {
-                    "type": "string",
-                    "default": "rgba(193, 223, 238, 1.0)"
-                },
-                "isabelle.warning_light_color": {
-                    "type": "string",
-                    "default": "rgba(255, 140, 0, 1.0)"
-                },
-                "isabelle.warning_dark_color": {
-                    "type": "string",
-                    "default": "rgba(255, 140, 0, 1.0)"
-                },
-                "isabelle.error_light_color": {
-                    "type": "string",
-                    "default": "rgba(178, 34, 34, 1.00)"
-                },
-                "isabelle.error_dark_color": {
-                    "type": "string",
-                    "default": "rgba(178, 34, 34, 1.00)"
-                },
-                "isabelle.spell_checker_light_color": {
-                    "type": "string",
-                    "default": "rgba(0, 0, 255, 1.0)"
-                },
-                "isabelle.spell_checker_dark_color": {
-                    "type": "string",
-                    "default": "rgba(86, 156, 214, 1.00)"
-                },
-                "isabelle.main_light_color": {
-                    "type": "string",
-                    "default": "rgba(0, 0, 0, 1.00)"
-                },
-                "isabelle.main_dark_color": {
-                    "type": "string",
-                    "default": "rgba(212, 212, 212, 1.00)"
-                },
-                "isabelle.keyword1_light_color": {
-                    "type": "string",
-                    "default": "rgba(175, 0, 219, 1.00)"
-                },
-                "isabelle.keyword1_dark_color": {
-                    "type": "string",
-                    "default": "rgba(197, 134, 192, 1.00)"
-                },
-                "isabelle.keyword2_light_color": {
-                    "type": "string",
-                    "default": "rgba(9, 136, 90, 1.00)"
-                },
-                "isabelle.keyword2_dark_color": {
-                    "type": "string",
-                    "default": "rgba(181, 206, 168, 1.00)"
+                "isabelle.always_open_thys": {
+                    "type": "boolean",
+                    "default": false,
+                    "description": "Always open '.thy' files as Isabelle theories."
                 },
-                "isabelle.keyword3_light_color": {
-                    "type": "string",
-                    "default": "rgba(38, 127, 153, 1.00)"
-                },
-                "isabelle.keyword3_dark_color": {
-                    "type": "string",
-                    "default": "rgba(78, 201, 176), 1.00)"
-                },
-                "isabelle.quasi_keyword_light_color": {
-                    "type": "string",
-                    "default": "rgba(153, 102, 255, 1.00)"
-                },
-                "isabelle.quasi_keyword_dark_color": {
-                    "type": "string",
-                    "default": "rgba(153, 102, 255, 1.00)"
-                },
-                "isabelle.improper_light_color": {
-                    "type": "string",
-                    "default": "rgba(205, 49, 49, 1.00)"
-                },
-                "isabelle.improper_dark_color": {
-                    "type": "string",
-                    "default": "rgba(244, 71, 71, 1.00)"
-                },
-                "isabelle.operator_light_color": {
-                    "type": "string",
-                    "default": "rgba(50, 50, 50, 1.00)"
-                },
-                "isabelle.operator_dark_color": {
-                    "type": "string",
-                    "default": "rgba(212, 212, 212, 1.00)"
-                },
-                "isabelle.tfree_light_color": {
-                    "type": "string",
-                    "default": "rgba(160, 32, 240, 1.00)"
-                },
-                "isabelle.tfree_dark_color": {
-                    "type": "string",
-                    "default": "rgba(160, 32, 240, 1.00)"
-                },
-                "isabelle.tvar_light_color": {
-                    "type": "string",
-                    "default": "rgba(160, 32, 240, 1.00)"
-                },
-                "isabelle.tvar_dark_color": {
-                    "type": "string",
-                    "default": "rgba(160, 32, 240, 1.00)"
-                },
-                "isabelle.free_light_color": {
-                    "type": "string",
-                    "default": "rgba(0, 0, 255, 1.00)"
-                },
-                "isabelle.free_dark_color": {
-                    "type": "string",
-                    "default": "rgba(86, 156, 214, 1.00)"
-                },
-                "isabelle.skolem_light_color": {
-                    "type": "string",
-                    "default": "rgba(210, 105, 30, 1.00)"
-                },
-                "isabelle.skolem_dark_color": {
-                    "type": "string",
-                    "default": "rgba(210, 105, 30, 1.00)"
-                },
-                "isabelle.bound_light_color": {
-                    "type": "string",
-                    "default": "rgba(0, 128, 0, 1.00)"
-                },
-                "isabelle.bound_dark_color": {
-                    "type": "string",
-                    "default": "rgba(96, 139, 78, 1.00)"
-                },
-                "isabelle.var_light_color": {
-                    "type": "string",
-                    "default": "rgba(0, 16, 128, 1.00)"
-                },
-                "isabelle.var_dark_color": {
-                    "type": "string",
-                    "default": "rgba(156, 220, 254, 1.00)"
-                },
-                "isabelle.inner_numeral_light_color": {
-                    "type": "string",
-                    "default": "rgba(9, 136, 90, 1.00)"
-                },
-                "isabelle.inner_numeral_dark_color": {
-                    "type": "string",
-                    "default": "rgba(181, 206, 168, 1.00)"
-                },
-                "isabelle.inner_quoted_light_color": {
-                    "type": "string",
-                    "default": "rgba(163, 21, 21, 1.00)"
-                },
-                "isabelle.inner_quoted_dark_color": {
-                    "type": "string",
-                    "default": "rgba(206, 145, 120, 1.00)"
-                },
-                "isabelle.inner_cartouche_light_color": {
-                    "type": "string",
-                    "default": "rgba(129, 31, 63, 1.00)"
-                },
-                "isabelle.inner_cartouche_dark_color": {
-                    "type": "string",
-                    "default": "rgba(209, 105, 105, 1.00)"
-                },
-                "isabelle.inner_comment_light_color": {
-                    "type": "string",
-                    "default": "rgba(0, 128, 0, 1.00)"
-                },
-                "isabelle.inner_comment_dark_color": {
-                    "type": "string",
-                    "default": "rgba(96, 139, 78, 1.00)"
-                },
-                "isabelle.comment1_light_color": {
-                    "type": "string",
-                    "default": "rgba(129, 31, 63, 1.00)"
-                },
-                "isabelle.comment1_dark_color": {
-                    "type": "string",
-                    "default": "rgba(100, 102, 149, 1.00)"
-                },
-                "isabelle.comment2_light_color": {
-                    "type": "string",
-                    "default": "rgba(209, 105, 105, 1.00)"
-                },
-                "isabelle.comment2_dark_color": {
-                    "type": "string",
-                    "default": "rgba(206, 155, 120, 1.00)"
-                },
-                "isabelle.comment3_light_color": {
-                    "type": "string",
-                    "default": "rgba(0, 128, 0, 1.00)"
-                },
-                "isabelle.comment3_dark_color": {
-                    "type": "string",
-                    "default": "rgba(96, 139, 78, 1.00)"
-                },
-                "isabelle.dynamic_light_color": {
-                    "type": "string",
-                    "default": "rgba(121, 94, 38, 1.00)"
-                },
-                "isabelle.dynamic_dark_color": {
-                    "type": "string",
-                    "default": "rgba(220, 220, 170, 1.00)"
-                },
-                "isabelle.class_parameter_light_color": {
-                    "type": "string",
-                    "default": "rgba(210, 105, 30, 1.00)"
-                },
-                "isabelle.class_parameter_dark_color": {
-                    "type": "string",
-                    "default": "rgba(210, 105, 30, 1.00)"
-                },
-                "isabelle.antiquote_light_color": {
-                    "type": "string",
-                    "default": "rgba(102, 0, 204, 1.00)"
-                },
-                "isabelle.antiquote_dark_color": {
-                    "type": "string",
-                    "default": "rgba(197, 134, 192, 1.00)"
-                },
-                "isabelle.raw_text_light_color": {
-                    "type": "string",
-                    "default": "rgba(102, 0, 204, 1.00)"
-                },
-                "isabelle.raw_text_dark_color": {
-                    "type": "string",
-                    "default": "rgba(197, 134, 192, 1.00)"
-                },
-                "isabelle.plain_text_light_color": {
-                    "type": "string",
-                    "default": "rgba(102, 0, 204, 1.00)"
-                },
-                "isabelle.plain_text_dark_color": {
-                    "type": "string",
-                    "default": "rgba(197, 134, 192, 1.00)"
+                "isabelle.text_color": {
+                    "type": "object",
+                    "additionalProperties": {
+                        "type": "string"
+                    },
+                    "default": {
+                        "unprocessed_light": "rgba(255, 160, 160, 1.00)",
+                        "unprocessed_dark": "rgba(97, 0, 97, 1.00)",
+                        "unprocessed1_light": "rgba(255, 160, 160, 0.20)",
+                        "unprocessed1_dark": "rgba(97, 0, 97, 0.20)",
+                        "running_light": "rgba(97, 0, 97, 1.00)",
+                        "running_dark": "rgba(255, 160, 160, 1.00)",
+                        "running1_light": "rgba(97, 0, 97, 0.40)",
+                        "running1_dark": "rgba(255, 160, 160, 0.40)",
+                        "canceled_light": "rgba(255, 106, 106, 0.40)",
+                        "canceled_dark": "rgba(255, 106, 106, 0.40)",
+                        "bad_light": "rgba(255, 106, 106, 0.40)",
+                        "bad_dark": "rgba(255, 106, 106, 0.40)",
+                        "intensify_light": "rgba(255, 204, 102, 0.40)",
+                        "intensify_dark": "rgba(204, 136, 0, 0.20)",
+                        "markdown_bullet1_light": "rgba(218, 254, 218, 1.00)",
+                        "markdown_bullet1_dark": "rgba(5, 199, 5, 0.20)",
+                        "markdown_bullet2_light": "rgba(255, 240, 204, 1.00)",
+                        "markdown_bullet2_dark": "rgba(204, 143, 0, 0.20)",
+                        "markdown_bullet3_light": "rgba(231, 231, 255, 1.00)",
+                        "markdown_bullet3_dark": "rgba(0, 0, 204, 0.20)",
+                        "markdown_bullet4_light": "rgba(255, 224, 240, 1.00)",
+                        "markdown_bullet4_dark": "rgba(204, 0, 105, 0.20)",
+                        "quoted_light": "rgba(139, 139, 139, 0.10)",
+                        "quoted_dark": "rgba(150, 150, 150, 0.15)",
+                        "antiquoted_light": "rgba(255, 200, 50, 0.10)",
+                        "antiquoted_dark": "rgba(255, 214, 102, 0.15)",
+                        "writeln_light": "rgba(192, 192, 192, 1.0)",
+                        "writeln_dark": "rgba(192, 192, 192, 1.0)",
+                        "information_light": "rgba(193, 223, 238, 1.0)",
+                        "information_dark": "rgba(193, 223, 238, 1.0)",
+                        "warning_light": "rgba(255, 140, 0, 1.0)",
+                        "warning_dark": "rgba(255, 140, 0, 1.0)",
+                        "error_light": "rgba(178, 34, 34, 1.00)",
+                        "error_dark": "rgba(178, 34, 34, 1.00)",
+                        "spell_checker_light": "rgba(0, 0, 255, 1.0)",
+                        "spell_checker_dark": "rgba(86, 156, 214, 1.00)",
+                        "main_light": "rgba(0, 0, 0, 1.00)",
+                        "main_dark": "rgba(212, 212, 212, 1.00)",
+                        "keyword1_light": "rgba(175, 0, 219, 1.00)",
+                        "keyword1_dark": "rgba(197, 134, 192, 1.00)",
+                        "keyword2_light": "rgba(9, 136, 90, 1.00)",
+                        "keyword2_dark": "rgba(181, 206, 168, 1.00)",
+                        "keyword3_light": "rgba(38, 127, 153, 1.00)",
+                        "keyword3_dark": "rgba(78, 201, 176), 1.00)",
+                        "quasi_keyword_light": "rgba(153, 102, 255, 1.00)",
+                        "quasi_keyword_dark": "rgba(153, 102, 255, 1.00)",
+                        "improper_light": "rgba(205, 49, 49, 1.00)",
+                        "improper_dark": "rgba(244, 71, 71, 1.00)",
+                        "operator_light": "rgba(50, 50, 50, 1.00)",
+                        "operator_dark": "rgba(212, 212, 212, 1.00)",
+                        "tfree_light": "rgba(160, 32, 240, 1.00)",
+                        "tfree_dark": "rgba(160, 32, 240, 1.00)",
+                        "tvar_light": "rgba(160, 32, 240, 1.00)",
+                        "tvar_dark": "rgba(160, 32, 240, 1.00)",
+                        "free_light": "rgba(0, 0, 255, 1.00)",
+                        "free_dark": "rgba(86, 156, 214, 1.00)",
+                        "skolem_light": "rgba(210, 105, 30, 1.00)",
+                        "skolem_dark": "rgba(210, 105, 30, 1.00)",
+                        "bound_light": "rgba(0, 128, 0, 1.00)",
+                        "bound_dark": "rgba(96, 139, 78, 1.00)",
+                        "var_light": "rgba(0, 16, 128, 1.00)",
+                        "var_dark": "rgba(156, 220, 254, 1.00)",
+                        "inner_numeral_light": "rgba(9, 136, 90, 1.00)",
+                        "inner_numeral_dark": "rgba(181, 206, 168, 1.00)",
+                        "inner_quoted_light": "rgba(163, 21, 21, 1.00)",
+                        "inner_quoted_dark": "rgba(206, 145, 120, 1.00)",
+                        "inner_cartouche_light": "rgba(129, 31, 63, 1.00)",
+                        "inner_cartouche_dark": "rgba(209, 105, 105, 1.00)",
+                        "inner_comment_light": "rgba(0, 128, 0, 1.00)",
+                        "inner_comment_dark": "rgba(96, 139, 78, 1.00)",
+                        "comment1_light": "rgba(129, 31, 63, 1.00)",
+                        "comment1_dark": "rgba(100, 102, 149, 1.00)",
+                        "comment2_light": "rgba(209, 105, 105, 1.00)",
+                        "comment2_dark": "rgba(206, 155, 120, 1.00)",
+                        "comment3_light": "rgba(0, 128, 0, 1.00)",
+                        "comment3_dark": "rgba(96, 139, 78, 1.00)",
+                        "dynamic_light": "rgba(121, 94, 38, 1.00)",
+                        "dynamic_dark": "rgba(220, 220, 170, 1.00)",
+                        "class_parameter_light": "rgba(210, 105, 30, 1.00)",
+                        "class_parameter_dark": "rgba(210, 105, 30, 1.00)",
+                        "antiquote_light": "rgba(102, 0, 204, 1.00)",
+                        "antiquote_dark": "rgba(197, 134, 192, 1.00)",
+                        "raw_text_light": "rgba(102, 0, 204, 1.00)",
+                        "raw_text_dark": "rgba(197, 134, 192, 1.00)",
+                        "plain_text_light": "rgba(102, 0, 204, 1.00)",
+                        "plain_text_dark": "rgba(197, 134, 192, 1.00)"
+                    }
                 }
             }
         }
     },
     "scripts": {
         "vscode:prepublish": "tsc -p ./",
-        "compile": "tsc -watch -p ./",
-        "postinstall": "node ./node_modules/vscode/bin/install"
+        "compile": "tsc -watch -p ./"
     },
     "devDependencies": {
         "@types/mocha": "^2.2.48",
         "@types/node": "^10.11.0",
+        "@types/vscode": "^1.34.0",
         "mocha": "^3.5.3",
-        "typescript": "^3.9.9",
-        "vscode": "^1.1.36"
+        "typescript": "^3.9.9"
     },
     "dependencies": {
         "vscode-languageclient": "~5.2.1",
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/abbreviations.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/abbreviations.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,142 @@
+'use strict';
+
+import { ExtensionContext, Range, TextDocumentContentChangeEvent, workspace, WorkspaceEdit } from 'vscode'
+import { Prefix_Tree } from './isabelle_filesystem/prefix_tree'
+import * as library from './library'
+import * as symbol from './symbol'
+
+const entries: Record<string, string> = {}
+const prefix_tree: Prefix_Tree = new Prefix_Tree()
+
+function register_abbreviations(data: symbol.Entry[], context: ExtensionContext)
+{
+  const [min_length, max_length] = set_abbrevs(data)
+  const alphanumeric_regex = /[^A-Za-z0-9 ]/
+  context.subscriptions.push(
+    workspace.onDidChangeTextDocument(e =>
+    {
+      const doc = e.document
+      const mode = library.get_replacement_mode()
+      if (
+        mode === 'none' ||
+        doc.languageId !== 'isabelle' ||
+        doc.uri.scheme !== 'isabelle'
+      ) { return; }
+      const edits = new WorkspaceEdit()
+
+      const changes = e.contentChanges.slice(0)
+      changes.sort((c1, c2) => c1.rangeOffset - c2.rangeOffset)
+
+      let c: TextDocumentContentChangeEvent
+      while (c = changes.pop()) {
+        if (c.rangeLength === 1 || library.has_newline(c.text)) {
+          return
+        }
+
+        const end_offset = c.rangeOffset + c.text.length +
+          changes.reduce((a,b) => a + b.text.length, 0)
+
+        if (end_offset < min_length) {
+          continue
+        }
+
+        const start_offset = end_offset < max_length ? 0 : end_offset - max_length
+
+        const end_pos = doc.positionAt(end_offset)
+        let start_pos = doc.positionAt(start_offset)
+        let range = new Range(start_pos, end_pos)
+        const text = library.reverse(doc.getText(range))
+
+        const node = prefix_tree.get_end_or_value(text)
+        if (!node || !node.value) {
+          continue
+        }
+
+        const word = node.get_word().join('')
+        if (mode === 'non-alphanumeric' && !alphanumeric_regex.test(word)) {
+          continue
+        }
+
+        start_pos = doc.positionAt(end_offset - word.length)
+        range = new Range(start_pos, end_pos)
+
+        edits.replace(doc.uri, range, node.value as string)
+      }
+
+      apply_edits(edits)
+    })
+  )
+}
+
+async function apply_edits(edit: WorkspaceEdit)
+{
+  await waitForNextTick()
+  await workspace.applyEdit(edit)
+}
+
+function waitForNextTick(): Promise<void> {
+  return new Promise((res) => setTimeout(res, 0));
+}
+
+function get_unique_abbrevs(data: symbol.Entry[]): Set<string>
+{
+  const unique = new Set<string>()
+  const non_unique = new Set<string>()
+  for (const {code, abbrevs} of data) {
+    for (const abbrev of abbrevs) {
+      if (abbrev.length === 1 || non_unique.has(abbrev)) {
+        continue
+      }
+
+      if (unique.has(abbrev)) {
+        non_unique.add(abbrev)
+        unique.delete(abbrev)
+        entries[abbrev] = undefined
+        continue
+      }
+
+
+      entries[abbrev] = String.fromCharCode(code)
+      unique.add(abbrev)
+    }
+  }
+  return unique
+}
+
+function set_abbrevs(data: symbol.Entry[]): [number, number]
+{
+  const unique = get_unique_abbrevs(data)
+
+  // Add white space to abbrevs which are prefix of other abbrevs
+  for (const a1 of unique) {
+    for (const a2 of unique) {
+      if (a1 === a2) {
+        continue
+      }
+
+      if (a2.startsWith(a1)) {
+        const val = entries[a1]
+        delete entries[a1]
+        entries[a1 + ' '] = val
+        break
+      }
+    }
+  }
+
+  let min_length: number
+  let max_length: number
+  for (const entry in entries) {
+    if (!min_length || min_length > entry.length)
+      min_length = entry.length
+
+    if (!max_length || max_length< entry.length)
+      max_length = entry.length
+
+    // add reverse because we check the abbrevs from the end
+    prefix_tree.insert(library.reverse(entry), entries[entry])
+  }
+
+  return [min_length, max_length]
+}
+
+export { register_abbreviations }
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -1,11 +1,12 @@
 'use strict';
 
 import * as timers from 'timers'
-import { window, OverviewRulerLane } from 'vscode'
-import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
-  TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
-import { Decoration } from './protocol'
+import {window, OverviewRulerLane, Uri} from 'vscode';
+import { Range, DecorationOptions, DecorationRenderOptions,
+  TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext } from 'vscode'
+import { Document_Decorations } from './protocol'
 import * as library from './library'
+import { Isabelle_FSP } from './isabelle_filesystem/isabelle_fsp'
 
 
 /* known decoration types */
@@ -35,7 +36,7 @@
   "warning"
 ]
 
-const text_colors = [
+export const text_colors = [
   "main",
   "keyword1",
   "keyword2",
@@ -159,34 +160,37 @@
 /* decoration for document node */
 
 type Content = Range[] | DecorationOptions[]
-const document_decorations = new Map<string, Map<string, Content>>()
+const document_decorations = new Map<Uri, Map<string, Content>>()
 
 export function close_document(document: TextDocument)
 {
-  document_decorations.delete(document.uri.toString())
+  document_decorations.delete(document.uri)
 }
 
-export function apply_decoration(decoration: Decoration)
+export function apply_decoration(decorations: Document_Decorations)
 {
-  const typ = types.get(decoration.type)
-  if (typ) {
-    const uri = Uri.parse(decoration.uri).toString()
-    const content: DecorationOptions[] = decoration.content.map(opt =>
-      {
-        const r = opt.range
-        return {
-          range: new Range(new Position(r[0], r[1]), new Position(r[2], r[3])),
-          hoverMessage: opt.hover_message
+  const uri = Isabelle_FSP.get_isabelle(Uri.parse(decorations.uri))
+
+  for (const decoration of decorations.entries) {
+    const typ = types.get(decoration.type)
+    if (typ) {
+      const content: DecorationOptions[] = decoration.content.map(opt =>
+        {
+          const r = opt.range
+          return {
+            range: new Range(r[0], r[1], r[2], r[3]),
+            hoverMessage: opt.hover_message
+          }
+        })
+
+      const document = document_decorations.get(uri) || new Map<string, Content>()
+      document.set(decoration.type, content)
+      document_decorations.set(uri, document)
+
+      for (const editor of window.visibleTextEditors) {
+        if (uri.toString === editor.document.uri.toString) {
+          editor.setDecorations(typ, content)
         }
-      })
-
-    const document = document_decorations.get(uri) || new Map<string, Content>()
-    document.set(decoration.type, content)
-    document_decorations.set(uri, document)
-
-    for (const editor of window.visibleTextEditors) {
-      if (uri === editor.document.uri.toString()) {
-        editor.setDecorations(typ, content)
       }
     }
   }
@@ -195,7 +199,7 @@
 export function update_editor(editor: TextEditor)
 {
   if (editor) {
-    const decorations = document_decorations.get(editor.document.uri.toString())
+    const decorations = document_decorations.get(editor.document.uri)
     if (decorations) {
       for (const [typ, content] of decorations) {
         editor.setDecorations(types.get(typ), content)
@@ -218,7 +222,7 @@
       touched_editors.push(editor)
     }
   }
-  touched_documents.clear
+  touched_documents.clear()
   touched_editors.forEach(update_editor)
 }
 
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -1,57 +1,71 @@
 'use strict';
 
-import * as path from 'path';
-import * as fs from 'fs';
+import * as path from 'path'
 import * as library from './library'
-import * as decorations from './decorations';
-import * as preview_panel from './preview_panel';
-import * as protocol from './protocol';
-import * as state_panel from './state_panel';
-import * as symbol from './symbol';
-import * as completion from './completion';
+import * as decorations from './decorations'
+import * as preview_panel from './preview_panel'
+import * as protocol from './protocol'
+import * as state_panel from './state_panel'
 import { Uri, TextEditor, ViewColumn, Selection, Position, ExtensionContext, workspace, window,
-  commands, languages } from 'vscode';
-import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind,
-  NotificationType } from 'vscode-languageclient';
+  commands, ProgressLocation } from 'vscode'
+import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-languageclient'
+import { register_abbreviations } from './abbreviations'
+import { Isabelle_FSP } from './isabelle_filesystem/isabelle_fsp'
+import { Output_View_Provider } from './output_view'
+import { register_script_decorations } from './script_decorations'
 
 
 let last_caret_update: protocol.Caret_Update = {}
 
-export function activate(context: ExtensionContext)
+export async function activate(context: ExtensionContext)
 {
-  const isabelle_home = library.get_configuration<string>("home")
-  const isabelle_args = library.get_configuration<Array<string>>("args")
-  const cygwin_root = library.get_configuration<string>("cygwin_root")
-
-
   /* server */
 
-  if (isabelle_home === "")
-    window.showErrorMessage("Missing user settings: isabelle.home")
-  else {
+  try {
+    const isabelle_home = library.getenv_strict("ISABELLE_HOME")
+
+    const workspace_dir = await Isabelle_FSP.register(context)
+    const roots = workspace.workspaceFile === undefined ? await workspace.findFiles("{ROOT,ROOTS}") : []
+
     const isabelle_tool = isabelle_home + "/bin/isabelle"
-    const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
+    const isabelle_args =
+      ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
+        .concat(library.get_configuration<Array<string>>("args"))
+        .concat(roots.length > 0 && workspace_dir !== undefined ? ["-D", workspace_dir] : [])
 
     const server_options: ServerOptions =
       library.platform_is_windows() ?
-        { command:
-            (cygwin_root === "" ? path.join(isabelle_home, "contrib", "cygwin") : cygwin_root) +
-            "/bin/bash",
-          args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } :
+        { command: library.getenv_strict("CYGWIN_ROOT") + "\\bin\\bash",
+          args: ["-l", isabelle_tool, "vscode_server"].concat(isabelle_args) } :
         { command: isabelle_tool,
-          args: ["vscode_server"].concat(standard_args, isabelle_args) };
+          args: ["vscode_server"].concat(isabelle_args) }
+
     const language_client_options: LanguageClientOptions = {
       documentSelector: [
-        { language: "isabelle", scheme: "file" },
+        { language: "isabelle", scheme: Isabelle_FSP.scheme },
         { language: "isabelle-ml", scheme: "file" },
         { language: "bibtex", scheme: "file" }
-      ]
-    };
+      ],
+      uriConverters: {
+        code2Protocol: uri => Isabelle_FSP.get_file(uri).toString(),
+        protocol2Code: value => Isabelle_FSP.get_isabelle(Uri.parse(value))
+      }
+    }
 
     const language_client =
       new LanguageClient("Isabelle", server_options, language_client_options, false)
 
 
+    window.withProgress({location: ProgressLocation.Notification, cancellable: false},
+      async (progress) =>
+        {
+          progress.report({
+            message: "Waiting for Isabelle server..."
+          })
+          await language_client.onReady()
+        })
+
+
     /* decorations */
 
     decorations.setup(context)
@@ -65,6 +79,11 @@
       language_client.onNotification(protocol.decoration_type, decorations.apply_decoration))
 
 
+    /* super-/subscript decorations */
+
+    register_script_decorations(context)
+
+
     /* caret handling */
 
     function update_caret()
@@ -78,8 +97,10 @@
           caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character }
       }
       if (last_caret_update !== caret_update) {
-        if (caret_update.uri)
+        if (caret_update.uri) {
+          caret_update.uri = Isabelle_FSP.get_file(Uri.parse(caret_update.uri)).toString()
           language_client.sendNotification(protocol.caret_update_type, caret_update)
+        }
         last_caret_update = caret_update
       }
     }
@@ -93,6 +114,7 @@
       }
 
       if (caret_update.uri) {
+        caret_update.uri = Isabelle_FSP.get_isabelle(Uri.parse(caret_update.uri)).toString()
         workspace.openTextDocument(Uri.parse(caret_update.uri)).then(document =>
         {
           const editor = library.find_file_editor(document.uri)
@@ -115,15 +137,14 @@
 
     /* dynamic output */
 
-    const dynamic_output = window.createOutputChannel("Isabelle Output")
-    context.subscriptions.push(dynamic_output)
-    dynamic_output.show(true)
-    dynamic_output.hide()
+    const provider = new Output_View_Provider(context.extensionUri)
+    context.subscriptions.push(
+      window.registerWebviewViewProvider(Output_View_Provider.view_type, provider))
 
     language_client.onReady().then(() =>
     {
       language_client.onNotification(protocol.dynamic_output_type,
-        params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) })
+        params => provider.update_content(params.content))
     })
 
 
@@ -144,23 +165,27 @@
     language_client.onReady().then(() => preview_panel.setup(context, language_client))
 
 
-    /* Isabelle symbols */
+    /* Isabelle symbols and abbreviations */
 
     language_client.onReady().then(() =>
     {
+      language_client.onNotification(protocol.session_theories_type,
+        async ({entries}) => await Isabelle_FSP.init_workspace(entries))
+
       language_client.onNotification(protocol.symbols_type,
-        params => symbol.setup(context, params.entries))
-      language_client.sendNotification(protocol.symbols_request_type)
-    })
-
+        params =>
+          {
+            //register_abbreviations(params.entries, context)
+            Isabelle_FSP.update_symbol_encoder(params.entries)
 
-    /* completion */
+            // request theories to load in isabelle file system
+            // after a valid symbol encoder is loaded
+            language_client.sendNotification(protocol.session_theories_request_type)
+          })
 
-    const completion_provider = new completion.Completion_Provider
-    for (const mode of ["isabelle", "isabelle-ml"]) {
-      context.subscriptions.push(
-        languages.registerCompletionItemProvider(mode, completion_provider))
-    }
+      language_client.sendNotification(protocol.symbols_request_type)
+
+    })
 
 
     /* spell checker */
@@ -185,6 +210,10 @@
 
     context.subscriptions.push(language_client.start())
   }
+  catch (exn) {
+    window.showErrorMessage(exn)
+  }
 }
 
+
 export function deactivate() { }
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,683 @@
+'use strict';
+
+import {
+  commands,
+  Disposable,
+  Event,
+  EventEmitter,
+  ExtensionContext,
+  FileChangeEvent,
+  FileChangeType,
+  FileStat,
+  FileSystemError,
+  FileSystemProvider,
+  FileType,
+  languages,
+  TextDocument,
+  Uri, ViewColumn,
+  window,
+  workspace
+} from 'vscode';
+import * as path from 'path';
+import {Symbol_Encoder} from './symbol_encoder';
+import {Session_Theories, session_theories_request_type} from '../protocol';
+import {State_Key, Workspace_State} from './workspace_state';
+import * as symbol from '../symbol'
+import * as library from '../library';
+import {Uri_Map} from './uri_map';
+
+export class File implements FileStat
+{
+  type: FileType
+  ctime: number
+  mtime: number
+  size: number
+
+  name: string
+  data?: Uint8Array
+
+  constructor(name: string)
+  {
+    this.type = FileType.File
+    this.ctime = Date.now()
+    this.mtime = Date.now()
+    this.size = 0
+    this.name = name
+  }
+}
+
+export class Directory implements FileStat
+{
+  type: FileType
+  ctime: number
+  mtime: number
+  size: number
+
+  name: string
+  entries: Map<string, File | Directory>
+
+  constructor(name: string)
+  {
+    this.type = FileType.Directory
+    this.ctime = Date.now()
+    this.mtime = Date.now()
+    this.size = 0
+    this.name = name
+    this.entries = new Map()
+  }
+}
+
+export type Entry = File | Directory
+
+export class Isabelle_FSP implements FileSystemProvider
+{
+  private static instance: Isabelle_FSP
+  private static state: Workspace_State
+  private static readonly draft_session = 'Draft'
+  private static readonly session_dir = 'Isabelle Sessions'
+
+  //#region public static API
+
+  public static readonly scheme = 'isabelle'
+  public static readonly isabelle_lang_id = 'isabelle'
+  public static readonly theory_extension = '.thy'
+  public static readonly theory_files_glob = '**/*.thy'
+
+  public static register(context: ExtensionContext): Promise<string|undefined>
+  {
+    this.instance = new Isabelle_FSP()
+    this.state = new Workspace_State(context)
+    context.subscriptions.push(
+      workspace.registerFileSystemProvider(this.scheme, this.instance),
+
+      workspace.onDidOpenTextDocument((doc) =>
+        this.instance.open_workspace_document(doc)),
+
+      window.onDidChangeActiveTextEditor(({ document}) =>
+        this.instance.active_document_dialogue(document)),
+
+      this.instance.sync_subscription(),
+
+      commands.registerTextEditorCommand('isabelle.reload-file',
+        ({document}) => this.instance.reload_document(document.uri))
+    )
+
+    return this.instance.setup_workspace()
+  }
+
+  public static async update_symbol_encoder(entries: symbol.Entry[])
+  {
+    this.instance.symbol_encoder = new Symbol_Encoder(entries)
+    await this.state.set(State_Key.symbol_entries, entries)
+  }
+
+  public static async init_workspace(sessions: Session_Theories[])
+  {
+    await this.instance.init_filesystem(sessions)
+    for (const doc of workspace.textDocuments) {
+      await this.instance.open_workspace_document(doc)
+    }
+    if (window.activeTextEditor) {
+      await this.instance.active_document_dialogue(window.activeTextEditor.document)
+    }
+  }
+
+  public static get_isabelle(file_uri: Uri): Uri
+  {
+    return this.instance.file_to_isabelle.get_to(file_uri) || file_uri
+  }
+
+  public static get_file(isabelle_uri: Uri): Uri
+  {
+    return this.instance.file_to_isabelle.get_from(isabelle_uri) || isabelle_uri
+  }
+
+  //#endregion
+
+
+  //#region subscriptions
+
+  public async open_workspace_document(doc: TextDocument)
+  {
+    if (doc.uri.scheme === Isabelle_FSP.scheme) {
+      if (doc.languageId !== Isabelle_FSP.isabelle_lang_id) {
+        languages.setTextDocumentLanguage(doc, Isabelle_FSP.isabelle_lang_id)
+      }
+    } else {
+      if (doc.languageId === Isabelle_FSP.isabelle_lang_id) {
+        const isabelle_uri = this.file_to_isabelle.get_to(doc.uri)
+        if (!isabelle_uri) {
+          await this.create_mapping_load_theory(doc.uri)
+        } else if (!this.is_open_theory(isabelle_uri)) {
+          await this.load_theory(doc.uri, isabelle_uri)
+        }
+      }
+    }
+  }
+
+  public async active_document_dialogue(doc: TextDocument)
+  {
+    if (doc.uri.scheme === Isabelle_FSP.scheme) {
+      if (!await this.is_workspace_theory(doc.uri)) {
+        Isabelle_FSP.warn_not_synchronized(doc.fileName)
+      }
+    } else if (doc.fileName.endsWith(Isabelle_FSP.theory_extension)) {
+      const isabelle_uri = this.file_to_isabelle.get_to(doc.uri)
+      if (!isabelle_uri || !this.is_open_theory(isabelle_uri)) {
+        await this.open_theory_dialogue(doc.uri)
+      }
+    }
+  }
+
+  public sync_subscription(): Disposable
+  {
+    const watcher = workspace.createFileSystemWatcher(Isabelle_FSP.theory_files_glob)
+    watcher.onDidChange(file => this.reload_file_theory(file))
+    watcher.onDidDelete(file => this._delete(this.file_to_isabelle.get_to(file)))
+    return watcher
+  }
+
+  public async reload_document(doc: Uri)
+  {
+    if (doc.scheme === Isabelle_FSP.scheme) {
+      const file_uri = this.file_to_isabelle.get_from(doc)
+      await this.reload_theory(file_uri, doc)
+    }
+  }
+
+  public async reload_file_theory(file_uri: Uri)
+  {
+    const isabelle_uri = this.file_to_isabelle.get_to(file_uri)
+    await this.reload_theory(file_uri, isabelle_uri)
+  }
+
+  //#endregion
+
+
+  private symbol_encoder: Symbol_Encoder
+  private root = new Directory('')
+  private file_to_isabelle = new Uri_Map()
+  private session_theories: Session_Theories[] = []
+
+
+  //#region util
+
+  private static get_dir_uri(session: string): Uri
+  {
+    return Uri.parse(`${Isabelle_FSP.scheme}:/${session}`)
+  }
+  private static get_uri(session: string, rel_path: String): Uri
+  {
+    return Uri.parse(`${Isabelle_FSP.scheme}:/${session}/${rel_path}`)
+  }
+
+  //#endregion
+
+
+  //#region initialization
+
+  private async setup_workspace(): Promise<string|undefined>
+  {
+    const { state } = Isabelle_FSP
+    let { sessions, workspace_dir, symbol_entries } = state.get_setup_data()
+
+    const workspace_folders = workspace.workspaceFolders || []
+    const isabelle_folder = workspace_folders.find(folder =>
+       folder.name === Isabelle_FSP.session_dir && folder.uri.scheme === Isabelle_FSP.scheme)
+
+    if (isabelle_folder === undefined) {
+      workspace.updateWorkspaceFolders(0, 0,
+        { uri: Isabelle_FSP.get_dir_uri(''), name: Isabelle_FSP.session_dir })
+    }
+
+    if (sessions && workspace_dir && symbol_entries) {
+      await Isabelle_FSP.update_symbol_encoder(symbol_entries)
+      await this.init_filesystem(sessions)
+    } else {
+      const default_folder = workspace_folders.find(folder => folder.uri.scheme !== Isabelle_FSP.scheme)
+      if (default_folder !== undefined) workspace_dir = default_folder.uri.fsPath
+    }
+
+    await state.set(State_Key.workspace_dir, workspace_dir)
+    await this.save_tree_state()
+    this.onDidChangeFile(events => {
+      for (const e of events) {
+        if (e.type === FileChangeType.Changed) continue
+
+        this.save_tree_state()
+        return
+      }
+    })
+    return workspace_dir
+  }
+
+  private async init_filesystem(sessions: Session_Theories[])
+  {
+    const all_theory_uris = sessions
+      .map(s => s.theories)
+      .reduce((acc,x) => acc.concat(x), [])
+
+    const root_entries = Array.from(this.root.entries.keys())
+
+    // clean old files
+    for (const key of root_entries) {
+      if (key === Isabelle_FSP.draft_session) {
+        const draft = this.root.entries.get(key)
+
+        if (draft instanceof Directory) {
+          for (const draft_thy of draft.entries.keys()) {
+            const isabelle_uri = Isabelle_FSP.get_uri(Isabelle_FSP.draft_session, draft_thy)
+            const file_uri = this.file_to_isabelle.get_from(isabelle_uri)
+
+            if (file_uri && all_theory_uris.includes(file_uri.toString())) {
+              this._delete(isabelle_uri)
+            }
+          }
+        }
+      } else {
+        this._delete(Isabelle_FSP.get_dir_uri(key), true)
+      }
+    }
+
+    // create new
+    for (const { session_name, theories: theories_uri } of sessions) {
+      if (!session_name) continue
+      if (session_name !== Isabelle_FSP.draft_session) {
+        this.session_theories.push({
+          session_name,
+          theories: theories_uri.map(t => Uri.parse(t).toString())
+        })
+      }
+
+      if (!root_entries.includes(session_name)) {
+        this._create_directory(Isabelle_FSP.get_dir_uri(session_name))
+      }
+
+      for (const theory_uri of theories_uri) {
+        await this.create_mapping_load_theory(Uri.parse(theory_uri))
+      }
+    }
+  }
+
+  //#endregion
+
+
+  //#region fsp implementation
+
+  private _emitter = new EventEmitter<FileChangeEvent[]>()
+
+  readonly onDidChangeFile: Event<FileChangeEvent[]> = this._emitter.event
+
+  watch(_resource: Uri): Disposable
+  {
+    // ignore, fires for all changes...
+    return new Disposable(() => { })
+  }
+
+  stat(uri: Uri): FileStat
+  {
+    return this._lookup(uri, false)
+  }
+
+  readDirectory(uri: Uri): [string, FileType][]
+  {
+    const entry = this._lookup_directory(uri, false)
+    const result: [string, FileType][] = []
+    for (const [name, child] of entry.entries) {
+      result.push([name, child.type])
+    }
+    return result
+  }
+
+  createDirectory(uri: Uri): void
+  {
+    throw FileSystemError.NoPermissions('No permission to create on Isabelle File System')
+  }
+
+  readFile(uri: Uri): Uint8Array
+  {
+    const data = this._lookup_file(uri, false).data
+    if (data) {
+      return data
+    }
+    throw FileSystemError.FileNotFound()
+  }
+
+  async writeFile(isabelle_uri: Uri, content: Uint8Array, options: { create: boolean, overwrite: boolean }): Promise<void>
+  {
+    if (!this.symbol_encoder) return
+    if (!this.file_to_isabelle.get_from(isabelle_uri)) {
+      throw FileSystemError.NoPermissions('No permission to create on Isabelle File System')
+    }
+
+    const basename = path.posix.basename(isabelle_uri.path)
+    const [parent, parent_uri] = this._get_parent_data(isabelle_uri)
+    let entry = parent.entries.get(basename)
+    if (entry instanceof Directory) {
+      throw FileSystemError.FileIsADirectory(isabelle_uri)
+    }
+    if (!entry && !options.create) {
+      throw FileSystemError.FileNotFound(isabelle_uri)
+    }
+    if (entry && options.create && !options.overwrite) {
+      throw FileSystemError.FileExists(isabelle_uri)
+    }
+
+    if (entry) {
+      if (options.create) {
+        return this.sync_original(isabelle_uri, content)
+      }
+
+      entry.mtime = Date.now()
+      entry.size = content.byteLength
+      entry.data = content
+
+      this._fire_soon({ type: FileChangeType.Changed, uri: isabelle_uri })
+      return
+    }
+
+    entry = new File(basename)
+    entry.mtime = Date.now()
+    entry.size = content.byteLength
+    entry.data = content
+
+    parent.entries.set(basename, entry)
+    parent.mtime = Date.now()
+    parent.size++
+    this._fire_soon(
+      { type: FileChangeType.Changed, uri: parent_uri },
+      { type: FileChangeType.Created, uri: isabelle_uri }
+    )
+  }
+
+  delete(uri: Uri): void
+  {
+    const [parent, parent_uri] = this._get_parent_data(uri)
+    if (parent && parent.name === Isabelle_FSP.draft_session) {
+      if (parent.size === 1) {
+        this._delete(parent_uri)
+        return
+      }
+
+      this._delete(uri)
+      return
+    }
+
+    throw FileSystemError.NoPermissions('No permission to delete on Isabelle File System')
+  }
+
+  rename(oldUri: Uri, newUri: Uri, options: { overwrite: boolean }): void
+  {
+    throw FileSystemError.NoPermissions('No permission to rename on Isabelle File System')
+  }
+
+  //#endregion
+
+
+  //#region implementation
+
+  private is_open_theory(isabelle_uri: Uri): boolean
+  {
+    const open_files = workspace.textDocuments
+    return !!(open_files.find((doc) => doc.uri.toString() === isabelle_uri.toString()))
+  }
+
+  private async load_theory(file_uri: Uri, isabelle_uri: Uri)
+  {
+    if (!this.symbol_encoder) return
+    const data = await workspace.fs.readFile(file_uri)
+    const encoded_data = this.symbol_encoder.encode(data)
+    await this.writeFile(isabelle_uri, encoded_data, { create: true, overwrite: true })
+  }
+
+  private async create_mapping_load_theory(file_uri: Uri): Promise<Uri>
+  {
+    const session = this.get_session(file_uri)
+    const isabelle_uri = this.create_new_uri(file_uri, session)
+    this.file_to_isabelle.add(file_uri, isabelle_uri)
+
+    await this.load_theory(file_uri, isabelle_uri)
+    return isabelle_uri
+  }
+
+  private async is_workspace_theory(isabelle_uri: Uri): Promise<boolean>
+  {
+    const file_uri = this.file_to_isabelle.get_from(isabelle_uri)
+    const files = await workspace.findFiles(Isabelle_FSP.theory_files_glob)
+    return !!(files.find(uri => uri.toString() === file_uri.toString()))
+  }
+
+  private static warn_not_synchronized(file_name: string)
+  {
+     window.showWarningMessage(`Theory ${file_name} not in workspace.
+      Changes to underlying theory file will be overwritten.`)
+  }
+
+  private async open_theory_dialogue(file_uri: Uri)
+  {
+    if (!this.symbol_encoder) return
+    const always_open = library.get_configuration<boolean>('always_open_thys')
+    if (!always_open) {
+      const answer = await window.showInformationMessage(
+        'Would you like to open the Isabelle theory associated with this file?',
+        'Yes',
+        'Always yes'
+      )
+      if (answer === 'Always yes') {
+        library.set_configuration('always_open_thys', true)
+      } else if (answer !== 'Yes') {
+        return
+      }
+    }
+
+    const isabelle_uri = await this.create_mapping_load_theory(file_uri)
+    await commands.executeCommand('vscode.open', isabelle_uri, ViewColumn.Active)
+  }
+
+  private async reload_theory(file_uri: Uri, isabelle_uri: Uri)
+  {
+    if (!this.symbol_encoder) return
+    const data = await workspace.fs.readFile(file_uri)
+    const encoded_data = this.symbol_encoder.encode(data)
+    await this.writeFile(isabelle_uri, encoded_data, { create: false, overwrite: true })
+  }
+
+  public get_session(file_uri: Uri): string
+  {
+    let session = this.session_theories.find((s) => s.theories.includes(file_uri.toString()))
+    if (!session) {
+      if (!this.root.entries.get(Isabelle_FSP.draft_session)) {
+        this._create_directory(Isabelle_FSP.get_uri(Isabelle_FSP.draft_session, ''))
+      }
+      return Isabelle_FSP.draft_session
+    }
+
+    return session.session_name
+  }
+
+  private create_new_uri(file_uri: Uri, session_name: string): Uri
+  {
+    const file_name = path.basename(file_uri.fsPath, Isabelle_FSP.theory_extension)
+    let new_uri: Uri
+    let extra = ''
+    let fs_path = file_uri.fsPath
+    while (true) {
+      const discriminator = extra ? ` (${extra})` : ''
+      new_uri = Isabelle_FSP.get_uri(session_name, file_name + discriminator)
+
+      const old_uri = this.file_to_isabelle.get_from(new_uri)
+      if (!old_uri || old_uri.toString() === file_uri.toString()) {
+        return new_uri
+      }
+
+      if (fs_path === '/') {
+        throw FileSystemError.FileExists(new_uri)
+      }
+
+      fs_path = path.posix.dirname(fs_path)
+      extra = path.posix.join(path.posix.basename(fs_path), extra)
+    }
+  }
+
+  private async save_tree_state()
+  {
+    const sessions: Session_Theories[] = []
+    for (const [session_name, val] of this.root.entries) {
+      if (!(val instanceof Directory)) return
+      const theories: string[] = []
+
+      for (const fileName of val.entries.keys()) {
+        const file = this.file_to_isabelle.get_from(Isabelle_FSP.get_uri(session_name, fileName))
+        theories.push(file.toString())
+      }
+
+      sessions.push({session_name, theories})
+    }
+
+    await Isabelle_FSP.state.set(State_Key.sessions, sessions)
+  }
+
+  private sync_deletion(isabelle_uri: Uri, silent: boolean)
+  {
+    const dir = this._lookup(isabelle_uri, silent)
+    if (!dir) {
+      if (silent)
+        return
+      else
+        throw FileSystemError.FileNotFound(isabelle_uri)
+    }
+
+    const uri_string = isabelle_uri.toString()
+    if (dir instanceof Directory) {
+      for (const key of dir.entries.keys()) {
+        this.remove_mapping(Uri.parse(uri_string + `/${key}`))
+      }
+    }
+    this.remove_mapping(isabelle_uri)
+  }
+
+  private remove_mapping(isabelle_uri: Uri)
+  {
+    const file = this.file_to_isabelle.get_from(isabelle_uri)
+    if (file) {
+      this.file_to_isabelle.delete(file, isabelle_uri)
+    }
+  }
+
+  private async sync_original(uri: Uri, content: Uint8Array)
+  {
+    if (!this.symbol_encoder) return
+    const origin_uri = this.file_to_isabelle.get_from(uri)
+    const decoded_content = this.symbol_encoder.decode(content)
+    workspace.fs.writeFile(origin_uri, decoded_content)
+  }
+
+  private _delete(uri: Uri, silent: boolean = false): void
+  {
+    const dirname = uri.with({ path: path.posix.dirname(uri.path) })
+    const basename = path.posix.basename(uri.path)
+    const parent = this._lookup_directory(dirname, silent)
+
+    if (!parent) return
+    if (!parent.entries.has(basename)) {
+      if (!silent)
+        throw FileSystemError.FileNotFound(uri)
+      else
+        return
+    }
+
+    this.sync_deletion(uri, silent)
+    parent.entries.delete(basename)
+    parent.mtime = Date.now()
+    parent.size -= 1
+
+    this._fire_soon({ type: FileChangeType.Changed, uri: dirname }, { uri, type: FileChangeType.Deleted })
+  }
+
+  private _create_directory(uri: Uri): void
+  {
+    const basename = path.posix.basename(uri.path)
+    const [parent, parent_uri] = this._get_parent_data(uri)
+
+    const entry = new Directory(basename)
+    parent.entries.set(entry.name, entry)
+    parent.mtime = Date.now()
+    parent.size += 1
+    this._fire_soon(
+      { type: FileChangeType.Changed, uri: parent_uri },
+      { type: FileChangeType.Created, uri }
+    )
+  }
+
+  private _get_parent_data(uri: Uri): [Directory, Uri]
+  {
+    const parent_uri = uri.with({ path: path.posix.dirname(uri.path) })
+    const parent = this._lookup_directory(parent_uri, false)
+
+    return [parent, parent_uri]
+  }
+
+  // --- lookup
+
+  private _lookup(uri: Uri, silent: false): Entry
+  private _lookup(uri: Uri, silent: boolean): Entry | undefined
+  private _lookup(uri: Uri, silent: boolean): Entry | undefined {
+    const parts = uri.path.split('/')
+    let entry: Entry = this.root
+    for (const part of parts) {
+      if (!part) {
+        continue
+      }
+      let child: Entry | undefined
+      if (entry instanceof Directory) {
+        child = entry.entries.get(part)
+      }
+      if (!child) {
+        if (!silent) {
+          throw FileSystemError.FileNotFound(uri)
+        } else {
+          return undefined
+        }
+      }
+      entry = child
+    }
+    return entry
+  }
+
+  private _lookup_directory(uri: Uri, silent: boolean): Directory
+  {
+    const entry = this._lookup(uri, silent)
+    if (entry instanceof Directory) {
+      return entry
+    }
+    throw FileSystemError.FileNotADirectory(uri)
+  }
+
+  private _lookup_file(uri: Uri, silent: boolean): File
+  {
+    const entry = this._lookup(uri, silent)
+    if (entry instanceof File) {
+      return entry
+    }
+    throw FileSystemError.FileIsADirectory(uri)
+  }
+
+  // --- manage file events
+
+  private _buffered_events: FileChangeEvent[] = []
+  private _fire_soon_handle?: NodeJS.Timer
+
+  private _fire_soon(...events: FileChangeEvent[]): void
+  {
+    this._buffered_events.push(...events)
+
+    if (this._fire_soon_handle) {
+      clearTimeout(this._fire_soon_handle)
+    }
+
+    this._fire_soon_handle = setTimeout(() => {
+      this._emitter.fire(this._buffered_events)
+      this._buffered_events.length = 0
+    }, 5)
+  }
+}
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/isabelle_filesystem/prefix_tree.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/prefix_tree.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,92 @@
+'use strict';
+
+class Tree_Node
+{
+  public key: number | string
+  public parent: Tree_Node = null
+  public end: boolean = false
+  public value: number[] | string
+  public children: Record<number | string, Tree_Node> = {}
+  constructor(key: number | string)
+  {
+    this.key = key
+  }
+
+  public get_word(): number[] | string[]
+  {
+    let output = []
+    let node: Tree_Node = this
+
+    while (node.key !== null) {
+      output.unshift(node.key)
+      node = node.parent
+    }
+
+    return output
+  }
+}
+
+class Prefix_Tree
+{
+  private root: Tree_Node
+
+  constructor()
+  {
+    this.root = new Tree_Node(null)
+  }
+
+  public insert(word: number[] | string, value: number[] | string)
+  {
+    let node = this.root
+    for (var i = 0; i < word.length; i++) {
+      if (!node.children[word[i]]) {
+        node.children[word[i]] = new Tree_Node(word[i])
+
+        node.children[word[i]].parent = node
+      }
+
+      node = node.children[word[i]]
+      node.end = false
+
+      if (i === word.length-1) {
+        node.end = true
+        node.value = value
+      }
+    }
+  }
+
+  public get_node(prefix: number[] | string): Tree_Node | undefined
+  {
+    let node = this.root
+
+    for (let i = 0; i < prefix.length; i++) {
+      if (!node.children[prefix[i]]) {
+        return
+      }
+      node = node.children[prefix[i]]
+    }
+    return node
+  }
+
+  public get_end_or_value(prefix: number[] | string): Tree_Node | undefined
+  {
+    let node = this.root
+    let resNode: Tree_Node
+    for (let i = 0; i < prefix.length; i++) {
+      if (!node.children[prefix[i]]) {
+        return resNode
+      }
+      node = node.children[prefix[i]]
+      if (node.value) {
+        resNode = node
+      }
+
+      if (node.end) {
+        return node
+      }
+    }
+    return node
+  }
+}
+
+export { Prefix_Tree, Tree_Node }
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/isabelle_filesystem/symbol_encoder.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/symbol_encoder.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,88 @@
+'use strict';
+
+import { TextEncoder } from 'util'
+import * as symbol from '../symbol'
+import { Prefix_Tree, Tree_Node } from './prefix_tree'
+
+class Encode_Data
+{
+  prefix_tree: Prefix_Tree
+  min_length: number
+  max_length: number
+
+  constructor(origin: Uint8Array[], replacement: Uint8Array[])
+  {
+    this.prefix_tree = new Prefix_Tree()
+
+    for (let i = 0; i < origin.length; i++) {
+      const entry = origin[i]
+      if (!this.min_length || this.min_length > entry.length)
+        this.min_length = entry.length
+
+      if (!this.max_length || this.max_length< entry.length)
+        this.max_length = entry.length
+
+      this.prefix_tree.insert(Array.from(entry), Array.from(replacement[i]))
+    }
+  }
+}
+
+export class Symbol_Encoder
+{
+  private symbols: Encode_Data
+  private sequences: Encode_Data
+
+  constructor(entries: symbol.Entry[])
+  {
+    let syms: Uint8Array[] = []
+    let seqs: Uint8Array[] = []
+    const encoder = new TextEncoder()
+    for (const {symbol, code} of entries) {
+      seqs.push(encoder.encode(symbol))
+      syms.push(encoder.encode(String.fromCharCode(code)))
+    }
+    this.symbols = new Encode_Data(syms, seqs)
+    this.sequences = new Encode_Data(seqs, syms)
+  }
+
+  encode(content: Uint8Array): Uint8Array
+  {
+    return this.code(content, this.sequences, this.symbols)
+  }
+
+  decode(content: Uint8Array): Uint8Array
+  {
+    return this.code(content, this.symbols, this.sequences)
+  }
+
+  private code(content: Uint8Array, origin: Encode_Data, replacements: Encode_Data): Uint8Array
+  {
+    const result: number[] = []
+
+    for (let i = 0; i < content.length; i++) {
+      if (i > content.length - origin.min_length) {
+        result.push(content[i])
+        continue
+      }
+
+      let word: number[] = []
+      let node: Tree_Node
+      for (let j = i; j < i + origin.max_length; j++) {
+        word.push(content[j])
+        node = origin.prefix_tree.get_node(word)
+        if (!node || node.end) {
+          break
+        }
+      }
+
+      if (node && node.end) {
+        result.push(...(node.value as number[]))
+        i += word.length - 1
+        continue
+      }
+      result.push(content[i])
+    }
+
+    return new Uint8Array(result)
+  }
+}
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/isabelle_filesystem/uri_map.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/uri_map.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,38 @@
+'use strict';
+
+import {Uri} from 'vscode';
+
+export class Uri_Map
+{
+  private map = new Map<string, Uri>()
+  private rev_map = new Map<string, Uri>()
+
+  private static normalize(uri: Uri): Uri
+  {
+    return Uri.parse(uri.toString())
+  }
+
+  public add(from: Uri, to: Uri)
+  {
+    const norm_from = Uri_Map.normalize(from)
+    const norm_to = Uri_Map.normalize(to)
+    this.map.set(norm_from.toString(), norm_to)
+    this.rev_map.set(norm_to.toString(), norm_from)
+  }
+
+  public delete(from: Uri, to: Uri)
+  {
+    this.map.delete(Uri_Map.normalize(from).toString())
+    this.rev_map.delete(Uri_Map.normalize(to).toString())
+  }
+
+  public get_to(from: Uri): Uri
+  {
+    return this.map.get(Uri_Map.normalize(from).toString())
+  }
+
+  public get_from(to: Uri): Uri
+  {
+    return this.rev_map.get(Uri_Map.normalize(to).toString())
+  }
+}
\ No newline at end of file
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,52 @@
+'use strict';
+
+import { ExtensionContext } from 'vscode'
+import { Session_Theories } from '../protocol'
+import * as symbol from '../symbol'
+
+interface Setup_Data
+{
+  workspace_dir: string
+  sessions: Session_Theories[]
+  symbol_entries: symbol.Entry[]
+}
+
+enum State_Key
+{
+  workspace_dir = 'workspace_dir',
+  sessions = 'sessions',
+  symbol_entries = 'symbol_entries'
+}
+
+class Workspace_State
+{
+  constructor(private context: ExtensionContext) { }
+
+  public get_setup_data(): Setup_Data
+  {
+    return {
+      workspace_dir: this.get(State_Key.workspace_dir),
+      sessions: this.get<Session_Theories[]>(State_Key.sessions),
+      symbol_entries: this.get<symbol.Entry[]>(State_Key.symbol_entries)
+    }
+  }
+
+  public set_setup_date(setup_data: Setup_Data)
+  {
+    const {workspace_dir: workspace_dir, sessions } = setup_data
+    this.set(State_Key.workspace_dir, workspace_dir) // TODO await?
+    this.set(State_Key.sessions, sessions) // TODO await?
+  }
+
+  public get<T = string>(key: State_Key): T
+  {
+    return this.context.workspaceState.get(key)
+  }
+
+  public async set(key: State_Key, value: any)
+  {
+    await this.context.workspaceState.update(key, value)
+  }
+}
+
+export { Workspace_State, State_Key, Setup_Data }
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/library.ts
--- a/src/Tools/VSCode/extension/src/library.ts	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -1,7 +1,8 @@
 'use strict';
 
-import * as os from 'os';
-import { TextEditor, Uri, ViewColumn, workspace, window } from 'vscode'
+import * as os from 'os'
+import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode'
+import {Isabelle_FSP} from './isabelle_filesystem/isabelle_fsp'
 
 
 /* regular expressions */
@@ -11,6 +12,39 @@
   return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&")
 }
 
+/* strings */
+
+export function quote(s: string): string
+{
+  return "\"" + s + "\""
+}
+
+export function reverse(s: string): string
+{
+  return s.split("").reverse().join("")
+}
+
+export function has_newline(text: string)
+{
+  return text.includes("\n") || text.includes("\r")
+}
+
+
+/* settings environment */
+
+export function getenv(name: string): string
+{
+  const s = process.env[name]
+  return s || ""
+}
+
+export function getenv_strict(name: string): string
+{
+  const s = getenv(name)
+  if (s) return s
+  else throw new Error("Undefined Isabelle environment variable: " + quote(name))
+}
+
 
 /* platform information */
 
@@ -24,7 +58,7 @@
 
 export function is_file(uri: Uri): boolean
 {
-  return uri.scheme === "file"
+  return uri.scheme === "file" || uri.scheme === Isabelle_FSP.scheme
 }
 
 export function find_file_editor(uri: Uri): TextEditor | undefined
@@ -47,10 +81,20 @@
   return workspace.getConfiguration("isabelle").get<T>(name)
 }
 
+export function set_configuration<T>(name: string, configuration: T)
+{
+  workspace.getConfiguration("isabelle").update(name, configuration)
+}
+
+export function get_replacement_mode()
+{
+  return get_configuration<"none" | "non-alphanumeric" | "all">("replacement")
+}
+
 export function get_color(color: string, light: boolean): string
 {
-  const config = color + (light ? "_light" : "_dark") + "_color"
-  return get_configuration<string>(config)
+  const colors = get_configuration<object>("text_color")
+  return colors[color + (light ? "_light" : "_dark")]
 }
 
 
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/output_view.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/output_view.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,108 @@
+'use strict';
+
+import { WebviewViewProvider, WebviewView, Uri, WebviewViewResolveContext,
+   CancellationToken, window, Position, Selection, Webview} from 'vscode'
+import { text_colors } from './decorations'
+import * as library from './library'
+import * as path from 'path'
+import { Isabelle_FSP } from './isabelle_filesystem/isabelle_fsp'
+
+class Output_View_Provider implements WebviewViewProvider
+{
+
+  public static readonly view_type = 'isabelle-output'
+
+  private _view?: WebviewView
+  private content: string = ''
+
+  constructor(private readonly _extension_uri: Uri) { }
+
+  public resolveWebviewView(
+    view: WebviewView,
+    context: WebviewViewResolveContext,
+    _token: CancellationToken)
+  {
+    this._view = view
+
+    view.webview.options = {
+      // Allow scripts in the webview
+      enableScripts: true,
+
+      localResourceRoots: [
+        this._extension_uri
+      ]
+    }
+
+    view.webview.html = this._get_html(this.content)
+    view.webview.onDidReceiveMessage(async message =>
+  {
+      if (message.command === 'open') {
+        open_webview_link(message.link)
+      }
+    })
+  }
+
+  public update_content(content: string)
+  {
+    if (!this._view) {
+      this.content = content
+      return
+    }
+
+    this._view.webview.html = this._get_html(content)
+  }
+
+  private _get_html(content: string): string
+  {
+    return get_webview_html(content, this._view.webview, this._extension_uri.fsPath)
+  }
+}
+
+function open_webview_link(link: string)
+{
+  const uri = Uri.parse(link)
+  const line = Number(uri.fragment) || 0
+  const pos = new Position(line, 0)
+  const uri_no_fragment = uri.with({ fragment: '' })
+  const isabelle_uri = Isabelle_FSP.get_isabelle(uri_no_fragment)
+  window.showTextDocument(isabelle_uri, {
+    preserveFocus: false,
+    selection: new Selection(pos, pos)
+  })
+}
+
+function get_webview_html(content: string, webview: Webview, extension_path: string): string
+{
+  const script_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'main.js')))
+  const css_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'vscode.css')))
+
+  return `<!DOCTYPE html>
+    <html lang='en'>
+      <head>
+        <meta charset='UTF-8'>
+        <meta name='viewport' content='width=device-width, initial-scale=1.0'>
+        <link href='${css_uri}' rel='stylesheet' type='text/css'>
+        <style>
+        ${_get_decorations()}
+        </style>
+        <title>Output</title>
+      </head>
+      <body>
+        ${content}
+        <script src='${script_uri}'></script>
+      </body>
+    </html>`
+}
+
+function _get_decorations(): string
+{
+  let style: string = ''
+  for (const key of text_colors) {
+  style += `body.vscode-light .${key} { color: ${library.get_color(key, true)} }\n`
+  style += `body.vscode-dark .${key} { color: ${library.get_color(key, false)} }\n`
+  }
+
+  return style
+}
+
+export { Output_View_Provider, get_webview_html, open_webview_link }
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/protocol.ts
--- a/src/Tools/VSCode/extension/src/protocol.ts	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/protocol.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -1,26 +1,29 @@
 'use strict';
 
-import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions } from 'vscode'
-import { NotificationType } from 'vscode-languageclient';
+import { MarkdownString } from 'vscode'
+import { NotificationType } from 'vscode-languageclient'
 import * as symbol from './symbol'
 
-
 /* decorations */
 
-export interface DecorationOpts {
+export interface Decoration_Options {
   range: number[],
-  hover_message?: MarkedString | MarkedString[]
+  hover_message?: MarkdownString | MarkdownString[]
 }
 
 export interface Decoration
 {
-  uri: string,
-  "type": string,
-  content: DecorationOpts[]
+  "type": string
+  content: Decoration_Options[]
+}
+
+export interface Document_Decorations {
+  uri: string
+  entries: Decoration[]
 }
 
 export const decoration_type =
-  new NotificationType<Decoration, void>("PIDE/decoration")
+  new NotificationType<Document_Decorations, void>("PIDE/decoration")
 
 
 /* caret handling */
@@ -54,6 +57,7 @@
 {
   id: number
   content: string
+  auto_update: boolean
 }
 
 export const state_output_type =
@@ -114,6 +118,22 @@
 export const symbols_request_type =
   new NotificationType<void, void>("PIDE/symbols_request")
 
+export interface Entries<T>
+{
+  entries: T[]
+}
+
+export interface Session_Theories
+{
+  session_name: string
+  theories: string[]
+}
+
+export const session_theories_type =
+  new NotificationType<Entries<Session_Theories>, void>("PIDE/session_theories")
+
+export const session_theories_request_type =
+  new NotificationType<void, void>("PIDE/session_theories_request")
 
 /* spell checker */
 
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/script_decorations.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/script_decorations.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -0,0 +1,133 @@
+'use strict';
+
+import { DecorationRangeBehavior, ExtensionContext, Range,
+  TextDocument, TextEditor, window, workspace } from 'vscode'
+
+const arrows = {
+  sub: '⇩',
+  sup: '⇧',
+  sub_begin: '⇘',
+  sub_end: '⇙',
+  sup_begin: '⇗',
+  sup_end: '⇖'
+}
+const no_hide_list = [' ', '\n', '\r', ...Object.values(arrows)]
+
+function should_hide(next_char: string): boolean
+{
+  return !no_hide_list.includes(next_char)
+}
+
+function find_closing(close: string, text: string, open_index: number): number | undefined
+{
+  let close_index = open_index
+  let counter = 1
+  const open = text[open_index]
+  while (counter > 0) {
+    let c = text[++close_index]
+
+    if (c === undefined) return
+
+    if (c === open) {
+      counter++
+    }
+    else if (c === close) {
+      counter--
+    }
+  }
+  return close_index
+}
+
+
+
+function extract_ranges(doc: TextDocument)
+{
+  const text = doc.getText()
+  const hide_ranges: Range[] = []
+  const sup_ranges: Range[] = []
+  const sub_ranges: Range[] = []
+
+  for (let i = 0; i < text.length - 1; i++) {
+    switch (text[i]) {
+      case arrows.sup:
+      case arrows.sub:
+        if (should_hide(text[i + 1])) {
+          const pos_mid = doc.positionAt(i + 1)
+          hide_ranges.push(new Range(doc.positionAt(i), pos_mid));
+          (text[i] === arrows.sub ? sub_ranges : sup_ranges)
+            .push(new Range(pos_mid, doc.positionAt(i + 2)))
+          i++
+        }
+        break
+      case arrows.sup_begin:
+      case arrows.sub_begin:
+        const close = text[i] === arrows.sub_begin ? arrows.sub_end : arrows.sup_end
+        const script_ranges = text[i] === arrows.sub_begin ? sub_ranges : sup_ranges
+        const close_index = find_closing(close, text, i)
+
+        if (close_index && close_index - i > 1) {
+          const pos_start = doc.positionAt(i + 1)
+          const pos_end = doc.positionAt(close_index)
+          hide_ranges.push(
+            new Range(doc.positionAt(i), pos_start),
+            new Range(pos_end, doc.positionAt(close_index + 1))
+          )
+          script_ranges.push(new Range(pos_start, pos_end))
+          i = close_index
+        }
+        break
+      default:
+        break
+    }
+  }
+
+  return { hide_ranges: hide_ranges, superscript_ranges: sup_ranges, subscript_ranges: sub_ranges }
+}
+
+export function register_script_decorations(context: ExtensionContext)
+{
+  const hide = window.createTextEditorDecorationType({
+    textDecoration: 'none; font-size: 0.001em',
+    rangeBehavior: DecorationRangeBehavior.ClosedClosed
+  })
+
+  const superscript = window.createTextEditorDecorationType({
+    textDecoration: 'none; position: relative; top: -0.5em; font-size: 80%'
+  })
+
+  const subscript = window.createTextEditorDecorationType({
+    textDecoration: 'none; position: relative; bottom: -0.5em; font-size: 80%'
+  })
+
+  const set_editor_decorations = (editor: TextEditor, doc: TextDocument) =>
+    {
+      const { hide_ranges: hideRanges, superscript_ranges: superscriptRanges, subscript_ranges: subscriptRanges } = extract_ranges(doc)
+
+      editor.setDecorations(hide, hideRanges)
+      editor.setDecorations(superscript, superscriptRanges)
+      editor.setDecorations(subscript, subscriptRanges)
+    }
+
+  context.subscriptions.push(
+    hide, superscript, subscript,
+
+    window.onDidChangeActiveTextEditor(editor =>
+      {
+        if (!editor) {
+          return
+        }
+
+        const doc = editor.document
+        set_editor_decorations(editor, doc)
+      }),
+
+    workspace.onDidChangeTextDocument(({ document}) =>
+      {
+        for (const editor of window.visibleTextEditors) {
+          if (editor.document.uri.toString() === document.uri.toString()) {
+            set_editor_decorations(editor, document)
+          }
+        }
+      })
+  )
+}
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/state_panel.ts
--- a/src/Tools/VSCode/extension/src/state_panel.ts	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -2,8 +2,9 @@
 
 import * as library from './library'
 import * as protocol from './protocol'
-import { LanguageClient } from 'vscode-languageclient';
-import { Uri, ExtensionContext, window, WebviewPanel, ViewColumn } from 'vscode'
+import {LanguageClient} from 'vscode-languageclient'
+import {ExtensionContext, Uri, ViewColumn, WebviewPanel, window} from 'vscode'
+import {get_webview_html, open_webview_link} from './output_view'
 
 
 let language_client: LanguageClient
@@ -17,14 +18,15 @@
 {
   private state_id: number
   private webview_panel: WebviewPanel
+  private _extension_path: string
 
   public get_id(): number { return this.state_id }
   public check_id(id: number): boolean { return this.state_id === id }
 
-  public set_content(id: number, body: string)
+  public set_content(state: protocol.State_Output)
   {
-    this.state_id = id
-    this.webview_panel.webview.html = body
+    this.state_id = state.id
+    this.webview_panel.webview.html = this._get_html(state.content, state.auto_update)
   }
 
   public reveal()
@@ -32,34 +34,47 @@
     this.webview_panel.reveal(panel_column())
   }
 
-  constructor()
+  constructor(extension_path: string)
   {
-    this.webview_panel =
-      window.createWebviewPanel("isabelle-state", "State", panel_column(),
-        {
-          enableScripts: true
-        });
+    this._extension_path = extension_path
+    this.webview_panel = window.createWebviewPanel("isabelle-state", "State",
+      panel_column(), { enableScripts: true })
     this.webview_panel.onDidDispose(exit_panel)
     this.webview_panel.webview.onDidReceiveMessage(message =>
-      {
-        switch (message.command) {
-          case 'auto_update':
-            language_client.sendNotification(
-              protocol.state_auto_update_type, { id: this.state_id, enabled: message.enabled })
-            break;
+    {
+      switch (message.command) {
+        case "auto_update":
+          language_client.sendNotification(
+            protocol.state_auto_update_type, { id: this.state_id, enabled: message.enabled })
+          break
+        case "update":
+          language_client.sendNotification(protocol.state_update_type, { id: this.state_id })
+          break
+        case "locate":
+          language_client.sendNotification(protocol.state_locate_type, { id: this.state_id })
+          break
+        case "open":
+          open_webview_link(message.link)
+          break
+        default:
+          break
+      }
+    })
+  }
 
-          case 'update':
-            language_client.sendNotification(protocol.state_update_type, { id: this.state_id })
-            break;
+  private _get_html(content: string, auto_update: boolean): string
+  {
+    const webview = this.webview_panel.webview
+    const checked = auto_update ? "checked" : ""
+    const content_with_buttons = `<div id="controls">
+      <input type="checkbox" id="auto_update" ${checked}/>
+      <label for="auto_update">Auto update</label>
+      <button id="update_button">Update</button>
+      <button id="locate_button">Locate</button>
+    </div>
+    ${content}`
 
-          case 'locate':
-            language_client.sendNotification(protocol.state_locate_type, { id: this.state_id })
-            break;
-
-          default:
-            break;
-        }
-      })
+    return get_webview_html(content_with_buttons, webview, this._extension_path)
   }
 }
 
@@ -86,7 +101,9 @@
   language_client = client
   language_client.onNotification(protocol.state_output_type, params =>
     {
-      if (!panel) { panel = new Panel() }
-      panel.set_content(params.id, params.content)
+      if (!panel) {
+        panel = new Panel(context.extensionPath)
+      }
+      panel.set_content(params)
     })
 }
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -40,7 +40,8 @@
 {
   symbol: Symbol,
   name: string,
-  code: number
+  code: number,
+  abbrevs: string[]
 }
 
 let symbol_entries: [Entry]
@@ -73,75 +74,3 @@
     codes.set(entry.symbol, entry.code)
   }
 }
-
-
-/* prettify symbols mode */
-
-interface PrettyStyleProperties
-{
-  border?: string
-  textDecoration?: string
-  color?: string
-  backgroundColor?: string
-}
-
-interface PrettyStyle extends PrettyStyleProperties
-{
-  dark?: PrettyStyleProperties
-  light?: PrettyStyleProperties
-}
-
-interface Substitution
-{
-  ugly: string
-  pretty: string
-  pre?: string
-  post?: string
-  style?: PrettyStyle
-}
-
-interface LanguageEntry
-{
-  language: DocumentSelector
-  substitutions: Substitution[]
-}
-
-interface PrettifySymbolsMode
-{
-  onDidEnabledChange: (handler: (enabled: boolean) => void) => Disposable
-  isEnabled: () => boolean,
-  registerSubstitutions: (substitutions: LanguageEntry) => Disposable
-}
-
-export function setup(context: ExtensionContext, entries: [Entry])
-{
-  update_entries(entries)
-
-  const prettify_symbols_mode =
-    extensions.getExtension<PrettifySymbolsMode>("siegebell.prettify-symbols-mode")
-  if (prettify_symbols_mode) {
-    prettify_symbols_mode.activate().then(() =>
-    {
-      const substitutions: Substitution[] = []
-      for (const entry of names) {
-        const sym = entry[0]
-        substitutions.push(
-          {
-            ugly: library.escape_regex(sym),
-            pretty: library.escape_regex(get_unicode(sym))
-          })
-      }
-      for (const language of ["isabelle", "isabelle-ml", "isabelle-output"]) {
-        context.subscriptions.push(
-          prettify_symbols_mode.exports.registerSubstitutions(
-            {
-              language: language,
-              substitutions: substitutions
-            }))
-      }
-    })
-  }
-  else {
-    window.showWarningMessage("Please install extension \"Prettify Symbols Model\" and restart!")
-  }
-}
\ No newline at end of file
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/test/index.ts
--- a/src/Tools/VSCode/extension/test/index.ts	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/test/index.ts	Tue Feb 22 21:34:29 2022 +0100
@@ -15,7 +15,7 @@
 // You can directly control Mocha options by uncommenting the following lines
 // See https://github.com/mochajs/mocha/wiki/Using-mocha-programmatically#set-options for more info
 testRunner.configure({
-    ui: 'tdd', 		// the TDD UI is being used in extension.test.ts (suite, test, etc.)
+    ui: 'tdd',     // the TDD UI is being used in extension.test.ts (suite, test, etc.)
     useColors: true // colored output from test results
 });
 
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/extension/tsconfig.json
--- a/src/Tools/VSCode/extension/tsconfig.json	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/extension/tsconfig.json	Tue Feb 22 21:34:29 2022 +0100
@@ -9,6 +9,9 @@
         "sourceMap": true,
         "rootDir": "."
     },
+    "include": [
+        "src/**/*"
+    ],
     "exclude": [
         "node_modules",
         ".vscode-test"
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Tue Feb 22 21:34:29 2022 +0100
@@ -35,8 +35,25 @@
             else this
         }
       if (st1.output != output) {
-        channel.write(LSP.Dynamic_Output(
-          resources.output_pretty_message(Pretty.separate(st1.output))))
+        val elements = Presentation.Elements(
+          html = Presentation.elements2.html,
+          language = Presentation.elements2.language,
+          entity = Markup.Elements.full)
+
+        def entity_link(props: Properties.T, body: XML.Body): Option[XML.Tree] =
+          for {
+            thy_file <- Position.Def_File.unapply(props)
+            def_line <- Position.Def_Line.unapply(props)
+            source <- resources.source_file(thy_file)
+            uri = Path.explode(source).absolute_file.toURI
+          } yield HTML.link(uri.toString + "#" + def_line, body)
+
+        val htmlBody = Presentation.make_html(
+          Presentation.Entity_Context.empty,  // FIXME
+          elements,
+          Pretty.separate(st1.output))
+
+        channel.write(LSP.Dynamic_Output(HTML.source(htmlBody).toString))
       }
       st1
     }
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Tue Feb 22 21:34:29 2022 +0100
@@ -36,6 +36,7 @@
         var log_file: Option[Path] = None
         var logic_requirements = false
         var dirs: List[Path] = Nil
+        var select_dirs: List[Path] = Nil
         var include_sessions: List[String] = Nil
         var logic = default_logic
         var modes: List[String] = Nil
@@ -50,6 +51,7 @@
     -L FILE      logging on FILE
     -R NAME      build image with requirements from other sessions
     -d DIR       include session directory
+    -D DIR       include session directory and select its sessions (without build)
     -i NAME      include session in name-space of theories
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
     -m MODE      add print mode for output
@@ -62,6 +64,7 @@
           "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
           "R:" -> (arg => { logic = arg; logic_requirements = true }),
           "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
+          "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(File.standard_path(arg)))),
           "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
           "l:" -> (arg => logic = arg),
           "m:" -> (arg => modes = arg :: modes),
@@ -75,8 +78,9 @@
         val channel = new Channel(System.in, System.out, log, verbose)
         val server =
           new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
-            include_sessions = include_sessions, session_ancestor = logic_ancestor,
-            session_requirements = logic_requirements, modes = modes, log = log)
+            select_dirs = select_dirs, include_sessions = include_sessions,
+            session_ancestor = logic_ancestor, session_requirements = logic_requirements,
+            modes = modes, log = log)
 
         // prevent spurious garbage on the main protocol channel
         val orig_out = System.out
@@ -99,8 +103,9 @@
   val channel: Channel,
   options: Options,
   session_name: String = Language_Server.default_logic,
+  include_sessions: List[String] = Nil,
   session_dirs: List[Path] = Nil,
-  include_sessions: List[String] = Nil,
+  select_dirs: List[Path] = Nil,
   session_ancestor: Option[String] = None,
   session_requirements: Boolean = false,
   modes: List[String] = Nil,
@@ -213,6 +218,20 @@
   }
 
 
+  /* session structure */
+
+  def session_theories: Map[String, List[JFile]] =
+  {
+    val selection = Sessions.Selection.session(session_name)
+    val structure =
+      Sessions.load_structure(options, session_dirs, select_dirs).selection(selection)
+    for {
+      (name, base) <- Sessions.deps(structure).session_bases
+      sources = base.session_theories.map(_.path.file)
+    } yield (name, sources)
+  }
+
+
   /* output to client */
 
   private val delay_output: Delay =
@@ -265,13 +284,14 @@
       try {
         val base_info =
           Sessions.base_info(
-            options, session_name, dirs = session_dirs, include_sessions = include_sessions,
-            session_ancestor = session_ancestor, session_requirements = session_requirements).check
+            options, session_name, dirs = session_dirs ++ select_dirs,
+            include_sessions = include_sessions, session_ancestor = session_ancestor,
+            session_requirements = session_requirements).check
 
         def build(no_build: Boolean = false): Build.Results =
           Build.build(options,
-            selection = Sessions.Selection.session(base_info.session),
-            build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos)
+            selection = Sessions.Selection.session(base_info.session), build_heap = true,
+            no_build = no_build, dirs = session_dirs, infos = base_info.infos)
 
         if (!build(no_build = true).ok) {
           val start_msg = "Build started for Isabelle/" + base_info.session + " ..."
@@ -355,7 +375,7 @@
   {
     val result =
       (for ((rendering, offset) <- rendering_offset(node_pos))
-        yield rendering.completion(node_pos.pos, offset)) getOrElse Nil
+        yield rendering.completion(node_pos, offset)) getOrElse Nil
     channel.write(LSP.Completion.reply(id, result))
   }
 
@@ -466,6 +486,8 @@
           case LSP.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
           case LSP.Preview_Request(file, column) => request_preview(file, column)
           case LSP.Symbols_Request(()) => channel.write(LSP.Symbols())
+          case LSP.Session_Theories_Request(()) =>
+            channel.write(LSP.Session_Theories(session_theories))
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Tue Feb 22 21:34:29 2022 +0100
@@ -158,7 +158,11 @@
     val json: JSON.T =
       JSON.Object(
         "textDocumentSync" -> 2,
-        "completionProvider" -> JSON.Object("resolveProvider" -> false, "triggerCharacters" -> Nil),
+        "completionProvider" -> JSON.Object(
+          "resolveProvider" -> false,
+          "triggerCharacters" ->
+            Symbol.abbrevs.values.flatMap(_.iterator).map(_.toString).toList.distinct
+        ),
         "hoverProvider" -> true,
         "definitionProvider" -> true,
         "documentHighlightProvider" -> true)
@@ -212,6 +216,7 @@
     def unapply(json: JSON.T): Option[Line.Node_Range] =
       for {
         uri <- JSON.string(json, "uri")
+        if Url.is_wellformed_file(uri)
         range_json <- JSON.value(json, "range")
         range <- Range.unapply(range_json)
       } yield Line.Node_Range(Url.absolute_file_name(uri), range)
@@ -223,6 +228,7 @@
       for {
         doc <- JSON.value(json, "textDocument")
         uri <- JSON.string(doc, "uri")
+        if Url.is_wellformed_file(uri)
         pos_json <- JSON.value(json, "position")
         pos <- Position.unapply(pos_json)
       } yield Line.Node_Position(Url.absolute_file_name(uri), pos)
@@ -284,6 +290,7 @@
           for {
             doc <- JSON.value(params, "textDocument")
             uri <- JSON.string(doc, "uri")
+            if Url.is_wellformed_file(uri)
             lang <- JSON.string(doc, "languageId")
             version <- JSON.long(doc, "version")
             text <- JSON.string(doc, "text")
@@ -307,6 +314,7 @@
           for {
             doc <- JSON.value(params, "textDocument")
             uri <- JSON.string(doc, "uri")
+            if Url.is_wellformed_file(uri)
             version <- JSON.long(doc, "version")
             changes <- JSON.list(params, "contentChanges", unapply_change _)
           } yield (Url.absolute_file(uri), version, changes)
@@ -322,6 +330,7 @@
           for {
             doc <- JSON.value(params, "textDocument")
             uri <- JSON.string(doc, "uri")
+            if Url.is_wellformed_file(uri)
           } yield Url.absolute_file(uri)
         case _ => None
       }
@@ -501,11 +510,17 @@
       JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
   }
 
-  sealed case class Decoration(typ: String, content: List[DecorationOpts])
+  sealed case class Decoration(decorations: List[(String, List[DecorationOpts])])
   {
     def json(file: JFile): JSON.T =
       Notification("PIDE/decoration",
-        JSON.Object("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
+        JSON.Object(
+          "uri" -> Url.print_file(file),
+          "entries" -> decorations.map(decoration => JSON.Object(
+            "type" -> decoration._1,
+            "content" -> decoration._2.map(_.json))
+          ))
+      )
   }
 
 
@@ -549,8 +564,8 @@
 
   object State_Output
   {
-    def apply(id: Counter.ID, content: String): JSON.T =
-      Notification("PIDE/state_output", JSON.Object("id" -> id, "content" -> content))
+    def apply(id: Counter.ID, content: String, auto_update: Boolean): JSON.T =
+      Notification("PIDE/state_output", JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update))
   }
 
   class State_Id_Notification(name: String)
@@ -619,8 +634,27 @@
     {
       val entries =
         for ((sym, code) <- Symbol.codes)
-        yield JSON.Object("symbol" -> sym, "name" -> Symbol.names(sym)._1, "code" -> code)
+        yield JSON.Object(
+          "symbol" -> sym,
+          "name" -> Symbol.names(sym)._1,
+          "code" -> code,
+          "abbrevs" -> Symbol.abbrevs.get_list(sym)
+        )
       Notification("PIDE/symbols", JSON.Object("entries" -> entries))
     }
   }
+
+  /* Session structure */
+
+  object Session_Theories_Request extends Notification0("PIDE/session_theories_request")
+
+  object Session_Theories {
+    def apply(session_theories: Map[String, List[JFile]]): JSON.T = {
+      val entries = session_theories.map { case(session_name, theories) => JSON.Object(
+        "session_name" -> session_name,
+        "theories" -> theories.map(Url.print_file)
+      )}
+      Notification("PIDE/session_theories", JSON.Object("entries" -> entries))
+    }
+  }
 }
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala	Tue Feb 22 21:34:29 2022 +0100
@@ -52,7 +52,7 @@
   val id: Counter.ID = State_Panel.make_id()
 
   private def output(content: String): Unit =
-    server.channel.write(LSP.State_Output(id, content))
+    server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value))
 
 
   /* query operation */
@@ -61,17 +61,27 @@
 
   private val print_state =
     new Query_Operation(server.editor, (), "print_state", _ => (),
-      (snapshot, results, body) =>
-        if (output_active.value) {
-          val text = server.resources.output_pretty_message(Pretty.separate(body))
-          val content =
-            HTML.output_document(
-              List(HTML.style(HTML.fonts_css()),
-                HTML.style_file(HTML.isabelle_css),
-                HTML.script(controls_script)),
-              List(controls, HTML.source(text)),
-              css = "", structural = true)
-          output(content)
+      (_, _, body) =>
+        if (output_active.value && body.nonEmpty){
+          val elements = Presentation.Elements(
+            html = Presentation.elements2.html,
+            language = Presentation.elements2.language,
+            entity = Markup.Elements.full)
+
+          def entity_link(props: Properties.T, body: XML.Body): Option[XML.Tree] =
+            for {
+              thy_file <- Position.Def_File.unapply(props)
+              def_line <- Position.Def_Line.unapply(props)
+              source <- server.resources.source_file(thy_file)
+              uri = Path.explode(source).absolute_file.toURI
+            } yield HTML.link(uri.toString + "#" + def_line, body)
+
+          val htmlBody = Presentation.make_html(
+            Presentation.Entity_Context.empty,  // FIXME
+            elements,
+            Pretty.separate(body))
+
+          output(HTML.source(htmlBody).toString)
         })
 
   def locate(): Unit = print_state.locate_query()
@@ -105,44 +115,6 @@
   }
 
 
-  /* controls */
-
-  private def controls_script =
-"""
-const vscode = acquireVsCodeApi();
-
-function invoke_auto_update(enabled)
-{ vscode.postMessage({'command': 'auto_update', 'enabled': enabled}) }
-
-function invoke_update()
-{ vscode.postMessage({'command': 'update'}) }
-
-function invoke_locate()
-{ vscode.postMessage({'command': 'locate'}) }
-"""
-
-  private def auto_update_button: XML.Elem =
-    HTML.GUI.checkbox(HTML.text("Auto update"),
-      name = "auto_update",
-      tooltip = "Indicate automatic update following cursor movement",
-      selected = auto_update_enabled.value,
-      script = "invoke_auto_update(this.checked)")
-
-  private def update_button: XML.Elem =
-    HTML.GUI.button(List(HTML.bold(HTML.text("Update"))),
-      name = "update",
-      tooltip = "Update display according to the command at cursor position",
-      script = "invoke_update()")
-
-  private def locate_button: XML.Elem =
-    HTML.GUI.button(HTML.text("Locate"),
-      name = "locate",
-      tooltip = "Locate printed command within source text",
-      script = "invoke_locate()")
-
-  private def controls: XML.Elem =
-    HTML.Wrap_Panel(List(auto_update_button, update_button, locate_button))
-
 
   /* main */
 
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Feb 22 21:34:29 2022 +0100
@@ -86,10 +86,11 @@
 
   /* completion */
 
-  def completion(caret_pos: Line.Position, caret: Text.Offset): List[LSP.CompletionItem] =
+  def completion(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] =
   {
     val doc = model.content.doc
-    val line = caret_pos.line
+    val line = node_pos.pos.line
+    val unicode = node_pos.name.endsWith(".thy")
     doc.offset(Line.Position(line)) match {
       case None => Nil
       case Some(line_start) =>
@@ -98,13 +99,13 @@
 
         val syntax = model.syntax()
         val syntax_completion =
-          syntax.complete(history, unicode = false, explicit = true,
+          syntax.complete(history, unicode, explicit = false,
             line_start, doc.lines(line).text, caret - line_start,
             language_context(caret_range) getOrElse syntax.language_context)
 
         val (no_completion, semantic_completion) =
           rendering.semantic_completion_result(
-            history, false, syntax_completion.map(_.range), caret_range)
+            history, unicode, syntax_completion.map(_.range), caret_range)
 
         if (no_completion) Nil
         else {
@@ -121,8 +122,8 @@
               case Some(result) =>
                 result.items.map(item =>
                   LSP.CompletionItem(
-                    label = item.replacement,
-                    detail = Some(item.description.mkString(" ")),
+                    label = item.description.mkString(" "),
+                    text = Some(item.replacement),
                     range = Some(doc.range(item.range))))
             }
           items ::: VSCode_Spell_Checker.menu_items(rendering, caret)
@@ -234,16 +235,21 @@
             dotted(model.content.text_range)))).flatten :::
     List(VSCode_Spell_Checker.decoration(rendering))
 
-  def decoration_output(decoration: VSCode_Model.Decoration): LSP.Decoration =
+  def decoration_output(decoration: List[VSCode_Model.Decoration]): LSP.Decoration =
   {
-    val content =
-      for (Text.Info(text_range, msgs) <- decoration.content)
+    val entries =
+      for (deco <- decoration)
       yield {
-        val range = model.content.doc.range(text_range)
-        LSP.DecorationOpts(range,
-          msgs.map(msg => LSP.MarkedString(resources.output_pretty_tooltip(msg))))
+        val decopts = for(Text.Info(text_range, msgs) <- deco.content)
+          yield {
+            val range = model.content.doc.range(text_range)
+            LSP.DecorationOpts(range,
+              msgs.map(msg => LSP.MarkedString(resources.output_pretty_tooltip(msg))))
+          }
+        (deco.typ, decopts)
       }
-    LSP.Decoration(decoration.typ, content)
+
+    LSP.Decoration(entries)
   }
 
 
diff -r 18cd39e55eca -r 79fab5ff4163 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Feb 22 15:00:04 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Feb 22 21:34:29 2022 +0100
@@ -276,7 +276,7 @@
             file <- st.pending_input.iterator
             model <- st.models.get(file)
             (edits, model1) <-
-              model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file))
+              model.flush_edits(false, st.document_blobs, file, st.get_caret(file))
           } yield (edits, (file, model1))).toList
 
         for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
@@ -320,8 +320,8 @@
             for (diags <- changed_diags)
               channel.write(LSP.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
             if (pide_extensions) {
-              for (decos <- changed_decos; deco <- decos)
-                channel.write(rendering.decoration_output(deco).json(file))
+              for (decos <- changed_decos)
+                channel.write(rendering.decoration_output(decos).json(file))
             }
             (file, model1)
           }