vscode improvements: overhauled
authorFabian Huch <huch@in.tum.de>
Wed, 08 Sep 2021 16:53:16 +0200
changeset 74742 579789962c1c
parent 74741 84d9df6a2dc0
vscode improvements: overhauled
src/Tools/VSCode/extension/media/vscode.css
src/Tools/VSCode/extension/package-lock.json
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/abbreviations.ts
src/Tools/VSCode/extension/src/completion.ts
src/Tools/VSCode/extension/src/decorations.ts
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/isabelle_filesystem/isabelleFSP.ts
src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts
src/Tools/VSCode/extension/src/isabelle_filesystem/prefix_tree.ts
src/Tools/VSCode/extension/src/isabelle_filesystem/symbol_encoder.ts
src/Tools/VSCode/extension/src/isabelle_filesystem/workspaceState.ts
src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts
src/Tools/VSCode/extension/src/library.ts
src/Tools/VSCode/extension/src/output_view.ts
src/Tools/VSCode/extension/src/preview_panel.ts
src/Tools/VSCode/extension/src/protocol.ts
src/Tools/VSCode/extension/src/script_decorations.ts
src/Tools/VSCode/extension/src/state_panel.ts
src/Tools/VSCode/extension/test/index.ts
src/Tools/VSCode/src/dynamic_output.scala
src/Tools/VSCode/src/language_server.scala
src/Tools/VSCode/src/lsp.scala
src/Tools/VSCode/src/state_panel.scala
src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/extension/media/vscode.css	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/media/vscode.css	Wed Sep 08 16:53:16 2021 +0200
@@ -1,113 +1,113 @@
 :root {
-	--container-paddding: 20px;
-	--input-padding-vertical: 6px;
-	--input-padding-horizontal: 4px;
-	--input-margin-vertical: 4px;
-	--input-margin-horizontal: 0;
+  --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);
+  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);
+  padding-left: var(--container-paddding);
 }
 
 body > *,
 form > * {
-	margin-block-start: var(--input-margin-vertical);
-	margin-block-end: var(--input-margin-vertical);
+  margin-block-start: var(--input-margin-vertical);
+  margin-block-end: var(--input-margin-vertical);
 }
 
 *:focus {
-	outline-color: var(--vscode-focusBorder) !important;
+  outline-color: var(--vscode-focusBorder) !important;
 }
 
 a {
-	color: var(--vscode-textLink-foreground);
-	text-decoration: none;
+  color: var(--vscode-textLink-foreground);
+  text-decoration: none;
 }
 
 a:hover,
 a:active {
-	color: var(--vscode-textLink-activeForeground);
+  color: var(--vscode-textLink-activeForeground);
 }
 
 code {
-	font-size: var(--vscode-editor-font-size);
-	font-family: var(--vscode-editor-font-family);
+  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);
+  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);
+  cursor: pointer;
+  background: var(--vscode-button-hoverBackground);
 }
 
 button:focus {
-	outline-color: var(--vscode-focusBorder);
+  outline-color: var(--vscode-focusBorder);
 }
 
 button.secondary {
-	color: var(--vscode-button-secondaryForeground);
-	background: var(--vscode-button-secondaryBackground);
+  color: var(--vscode-button-secondaryForeground);
+  background: var(--vscode-button-secondaryBackground);
 }
 
 button.secondary:hover {
-	background: var(--vscode-button-secondaryHoverBackground);
+  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);
+  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);
+  color: var(--vscode-input-placeholderForeground);
 }
 
 #controls {
-	display: flex;
-	flex-direction: row;
-	justify-content: flex-end;
-	align-items: center;
+  display: flex;
+  flex-direction: row;
+  justify-content: flex-end;
+  align-items: center;
 }
 
 #controls > *{
-	margin-left: 5px;
-	margin-top: 5px;
+  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+ */
+  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
--- a/src/Tools/VSCode/extension/package-lock.json	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/package-lock.json	Wed Sep 08 16:53:16 2021 +0200
@@ -1,5 +1,5 @@
 {
-    "name": "Isabelle",
+    "name": "isabelle-vscode",
     "version": "1.2.2",
     "lockfileVersion": 1,
     "requires": true,
@@ -11,20 +11,21 @@
             "dev": true
         },
         "@types/node": {
-            "version": "10.17.58",
-            "resolved": "https://registry.npmjs.org/@types/node/-/node-10.17.58.tgz",
-            "integrity": "sha512-Dn5RBxLohjdHFj17dVVw3rtrZAeXeWg+LQfvxDIW/fdPkSiuQk7h3frKMYtsQhtIW42wkErDcy9UMVxhGW4O7w==",
+            "version": "10.17.60",
+            "resolved": "https://registry.npmjs.org/@types/node/-/node-10.17.60.tgz",
+            "integrity": "sha512-F0KIgDJfy2nA3zMLmWGKxcH2ZVEtCZXHHdOQs2gSaQ27+lNeEfGxzkIw90aXswATX7AZ33tahPbzy6KAfUreVw==",
             "dev": true
         },
         "@types/vscode": {
-            "version": "1.55.0",
-            "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.55.0.tgz",
-            "integrity": "sha512-49hysH7jneTQoSC8TWbAi7nKK9Lc5osQNjmDHVosrcU8o3jecD9GrK0Qyul8q4aGPSXRfNGqIp9CBdb13akETg=="
+            "version": "1.60.0",
+            "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.60.0.tgz",
+            "integrity": "sha512-wZt3VTmzYrgZ0l/3QmEbCq4KAJ71K3/hmMQ/nfpv84oH8e81KKwPEoQ5v8dNCxfHFVJ1JabHKmCvqdYOoVm1Ow==",
+            "dev": true
         },
         "balanced-match": {
-            "version": "1.0.0",
-            "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.0.tgz",
-            "integrity": "sha1-ibTRmasr7kneFk6gK4nORi1xt2c=",
+            "version": "1.0.2",
+            "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.2.tgz",
+            "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw==",
             "dev": true
         },
         "brace-expansion": {
@@ -272,26 +273,12 @@
                 "wrappy": "1"
             }
         },
-        "path": {
-            "version": "0.12.7",
-            "resolved": "https://registry.npmjs.org/path/-/path-0.12.7.tgz",
-            "integrity": "sha1-1NwqUGxM4hl+tIHr/NWzbAFAsQ8=",
-            "requires": {
-                "process": "^0.11.1",
-                "util": "^0.10.3"
-            }
-        },
         "path-is-absolute": {
             "version": "1.0.1",
             "resolved": "https://registry.npmjs.org/path-is-absolute/-/path-is-absolute-1.0.1.tgz",
             "integrity": "sha1-F0uSaHNVNP+8es5r9TpanhtcX18=",
             "dev": true
         },
-        "process": {
-            "version": "0.11.10",
-            "resolved": "https://registry.npmjs.org/process/-/process-0.11.10.tgz",
-            "integrity": "sha1-czIwDoQBYb2j5podHZGn1LwW8YI="
-        },
         "semver": {
             "version": "5.7.1",
             "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.1.tgz",
@@ -306,32 +293,12 @@
                 "has-flag": "^1.0.0"
             }
         },
-        "text-encoding": {
-            "version": "0.7.0",
-            "resolved": "https://registry.npmjs.org/text-encoding/-/text-encoding-0.7.0.tgz",
-            "integrity": "sha512-oJQ3f1hrOnbRLOcwKz0Liq2IcrvDeZRHXhd9RgLrsT+DjWY/nty1Hi7v3dtkaEYbPYe0mUoOfzRrMwfXXwgPUA=="
-        },
         "typescript": {
-            "version": "3.9.9",
-            "resolved": "https://registry.npmjs.org/typescript/-/typescript-3.9.9.tgz",
-            "integrity": "sha512-kdMjTiekY+z/ubJCATUPlRDl39vXYiMV9iyeMuEuXZh2we6zz80uovNN2WlAxmmdE/Z/YQe+EbOEXB5RHEED3w==",
+            "version": "3.9.10",
+            "resolved": "https://registry.npmjs.org/typescript/-/typescript-3.9.10.tgz",
+            "integrity": "sha512-w6fIxVE/H1PkLKcCPsFqKE7Kv7QUwhU8qQY2MueZXWx5cPZdwFupLgKK3vntcK98BtNHZtAF4LA/yl2a7k8R6Q==",
             "dev": true
         },
-        "util": {
-            "version": "0.10.4",
-            "resolved": "https://registry.npmjs.org/util/-/util-0.10.4.tgz",
-            "integrity": "sha512-0Pm9hTQ3se5ll1XihRic3FDIku70C+iHUdT/W926rSgHV5QgXsYbKZN8MSC3tJtSkhuROzvsQjAaFENRXr+19A==",
-            "requires": {
-                "inherits": "2.0.3"
-            },
-            "dependencies": {
-                "inherits": {
-                    "version": "2.0.3",
-                    "resolved": "https://registry.npmjs.org/inherits/-/inherits-2.0.3.tgz",
-                    "integrity": "sha1-Yzwsg+PaQqUC9SRmAiSA9CCCYd4="
-                }
-            }
-        },
         "vscode-jsonrpc": {
             "version": "4.0.0",
             "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-4.0.0.tgz",
--- a/src/Tools/VSCode/extension/package.json	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/package.json	Wed Sep 08 16:53:16 2021 +0200
@@ -25,35 +25,39 @@
     "activationEvents": [
         "workspaceContains:ROOT",
         "workspaceContains:ROOTS",
-		"onFileSystem:isabelle"
+        "onFileSystem:isabelle",
+        "onLanguage:isabelle",
+        "onCommand:isabelle.state",
+        "onCommand:isabelle.preview",
+        "onCommand:isabelle.preview-split",
+        "onCommand:isabelle.include-word",
+        "onCommand:isabelle.include-word-permanently",
+        "onCommand:isabelle.exclude-word",
+        "onCommand:isabelle.exclude-word-permanently",
+        "onCommand:isabelle.reset-words"
     ],
     "main": "./out/src/extension",
     "contributes": {
-		"viewsContainers": {
-		  "panel": [
-			{
-			  "id": "isabelle",
-			  "title": "Isabelle",
-			  "icon": ""
-			}
-		  ]
-		},
-		"views": {
-			"isabelle": [
-				{
-					"type": "webview",
-					"id": "isabelle-output",
-					"name": "Output"
-				}
-			]
-		},
+        "viewsContainers": {
+            "panel": [
+                {
+                    "id": "isabelle",
+                    "title": "Isabelle",
+                    "icon": ""
+                }
+            ]
+        },
+        "views": {
+            "isabelle": [
+                {
+                    "type": "webview",
+                    "id": "isabelle-output",
+                    "name": "Output"
+                }
+            ]
+        },
         "commands": [
             {
-                "command": "isabelle.reload-workspace",
-                "title": "Reload Workspace",
-                "category": "Isabelle"
-            },
-            {
                 "command": "isabelle.reload-file",
                 "title": "Reload File",
                 "category": "Isabelle"
@@ -217,19 +221,28 @@
                 },
                 "isabelle.replacement": {
                     "type": "string",
-                    "default": "non-alpha",
-                    "enum": ["none", "non-alpha", "all"],
+                    "default": "non-alphanumeric",
+                    "enum": [
+                        "none",
+                        "non-alphanumeric",
+                        "all"
+                    ],
                     "enumDescriptions": [
                         "Replacments are deactivated. No replacments are done.",
-                        "Replaces all uniqe abbreviations that contain no alpha numeric characters",
+                        "Replaces all uniqe abbreviations that contain no alphanumeric characters",
                         "Replaces all uniqe abbreviations"
                     ],
-                    "description": "Aggressive replacement mode"
+                    "description": "Symbol replacement mode."
                 },
-                "isabelle.textColor":{
+                "isabelle.always_open_thys": {
+                    "type": "boolean",
+                    "default": false,
+                    "description": "Always open '.thy' files as Isabelle theories."
+                },
+                "isabelle.text_color": {
                     "type": "object",
                     "additionalProperties": {
-                      "type": "string"
+                        "type": "string"
                     },
                     "default": {
                         "unprocessed_light": "rgba(255, 160, 160, 1.00)",
@@ -325,19 +338,16 @@
     },
     "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"
     },
     "dependencies": {
-        "@types/vscode": "^1.55.0",
-        "path": "^0.12.7",
-        "text-encoding": "^0.7.0",
         "vscode-languageclient": "~5.2.1",
         "vscode-languageserver-types": "~3.16.0"
     }
--- a/src/Tools/VSCode/extension/src/abbreviations.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/abbreviations.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,146 +1,142 @@
-import { ExtensionContext, Range, TextDocumentContentChangeEvent, workspace, WorkspaceEdit } from "vscode";
-import { PrefixTree } from "./isabelle_filesystem/prefix_tree";
-import { SymbolEntry } from "./isabelle_filesystem/symbol_encoder";
-import { get_replacement_mode } from "./library";
+'use strict';
 
-const entries: Record<string, string> = {};
-const prefixTree: PrefixTree = new PrefixTree();
+import { ExtensionContext, Range, TextDocumentContentChangeEvent, workspace, WorkspaceEdit } from 'vscode'
+import { Prefix_Tree } from './isabelle_filesystem/prefix_tree'
+import { Symbol_Entry } from './isabelle_filesystem/symbol_encoder'
+import * as library from './library'
+
+const entries: Record<string, string> = {}
+const prefix_tree: Prefix_Tree = new Prefix_Tree()
 
-function registerAbbreviations(data: SymbolEntry[], context: ExtensionContext){
-    const [minLength, maxLength] = setAbbrevs(data);
-    const regEx = /[^A-Za-z0-9 ]/;
-    context.subscriptions.push(
-        workspace.onDidChangeTextDocument(e => {
-            const doc = e.document;
-            const mode = get_replacement_mode();
-            if(
-                mode == 'none' ||
-                doc.languageId !== 'isabelle' || 
-                doc.uri.scheme !== 'isabelle'
-            ){
-                return;
-            }
-            const edits = new WorkspaceEdit();
+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);
+      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 || hasNewline(c.text)){
-                    return;
-                }
-                
-                const endOffset = c.rangeOffset + c.text.length + 
-                    changes.reduce((a,b) => a + b.text.length, 0);
-                
-                if(endOffset < minLength){
-                    continue;
-                }
+      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)
 
-                const beginOffset = endOffset < maxLength ? 0 : endOffset - maxLength;
+        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 endPos = doc.positionAt(endOffset);
-                let beginPos = doc.positionAt(beginOffset);
-                let range = new Range(beginPos, endPos);
-                const text = reverseString(doc.getText(range));
-                
-                const node = prefixTree.getEndOrValue(text);
-                if(!node || !node.value){
-                    continue;
-                }
+        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
+        }
 
-                const word = node.getWord().join('');
-                if(mode == 'non-alpha' && !regEx.test(word)){
-                    continue;
-                }
+        start_pos = doc.positionAt(end_offset - word.length)
+        range = new Range(start_pos, end_pos)
 
-                beginPos = doc.positionAt(endOffset - word.length);
-                range = new Range(beginPos, endPos);
+        edits.replace(doc.uri, range, node.value as string)
+      }
 
-                edits.replace(doc.uri, range, node.value as string);
-            }
-
-            applyEdits(edits);
-        })
-    );
+      apply_edits(edits)
+    })
+  )
 }
 
-async function applyEdits(edit: WorkspaceEdit){
-    await waitForNextTick();
-
-    await workspace.applyEdit(edit);
-}
-
-function getUniqueAbbrevs(data: SymbolEntry[]): Set<string>{
-    const unique = new Set<string>();
-    const nonUnique = new Set<string>();
-    for(const {symbol, code, abbrevs} of data){
-        for(const abbrev of abbrevs){
-            if(abbrev.length == 1 || nonUnique.has(abbrev)){
-                continue;
-            }
-
-            if(unique.has(abbrev)){
-                nonUnique.add(abbrev);
-                unique.delete(abbrev);
-                entries[abbrev] = undefined;
-                continue;
-            }
-
-
-            entries[abbrev] = String.fromCharCode(code);
-            unique.add(abbrev);
-        }
-    }
-    return unique;
-}
-
-function setAbbrevs(data: SymbolEntry[]): [number, number]{
-    const unique = getUniqueAbbrevs(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 minLength: number;
-    let maxLength: number;
-    for(const entry in entries){
-        if(!minLength || minLength > entry.length)
-            minLength = entry.length;
-        
-        if(!maxLength || maxLength< entry.length)
-            maxLength = entry.length;
-        
-        //add reverse because we check the abbrevs from the end
-        prefixTree.insert(reverseString(entry), entries[entry]);
-    }
-
-    return [minLength, maxLength];
-}
-
-function reverseString(str: string): string {
-    return str.split('').reverse().join('');
-}
-
-function hasNewline(text: string){
-    return text.includes('\n') || text.includes('\r');
+async function apply_edits(edit: WorkspaceEdit)
+{
+  await waitForNextTick()
+  await workspace.applyEdit(edit)
 }
 
 function waitForNextTick(): Promise<void> {
-	return new Promise((res) => setTimeout(res, 0));
+  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
 }
 
-export { registerAbbreviations };
\ No newline at end of file
+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 }
--- a/src/Tools/VSCode/extension/src/completion.ts	Fri Sep 03 15:03:29 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-'use strict';
-
-import { CompletionItemProvider, CompletionItem, TextDocument, Range, Position,
-  CancellationToken, CompletionList } from 'vscode'
-
-export class Completion_Provider implements CompletionItemProvider
-{
-  public provideCompletionItems(
-    document: TextDocument, position: Position, token: CancellationToken): CompletionList
-  {
-    const line_text = document.lineAt(position).text
-
-    return new CompletionList([])
-  }
-}
--- a/src/Tools/VSCode/extension/src/decorations.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,73 +1,73 @@
 'use strict';
 
 import * as timers from 'timers'
-import { window, OverviewRulerLane } from 'vscode'
+import {window, OverviewRulerLane, Uri} from 'vscode';
 import { Range, DecorationOptions, DecorationRenderOptions,
-  TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
-import { DocumentDecorations } from './protocol'
+  TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext } from 'vscode'
+import { Document_Decorations } from './protocol'
 import * as library from './library'
-import { IsabelleFSP } from './isabelle_filesystem/isabelleFSP';
+import { Isabelle_FSP } from './isabelle_filesystem/isabelle_fsp'
 
 
 /* known decoration types */
 
 const background_colors = [
-  "unprocessed1",
-  "running1",
-  "canceled",
-  "bad",
-  "intensify",
-  "quoted",
-  "antiquoted",
-  "markdown_bullet1",
-  "markdown_bullet2",
-  "markdown_bullet3",
-  "markdown_bullet4"
+  'unprocessed1',
+  'running1',
+  'canceled',
+  'bad',
+  'intensify',
+  'quoted',
+  'antiquoted',
+  'markdown_bullet1',
+  'markdown_bullet2',
+  'markdown_bullet3',
+  'markdown_bullet4'
 ]
 
 const foreground_colors = [
-  "quoted",
-  "antiquoted"
+  'quoted',
+  'antiquoted'
 ]
 
 const dotted_colors = [
-  "writeln",
-  "information",
-  "warning"
+  'writeln',
+  'information',
+  'warning'
 ]
 
 export const text_colors = [
-  "main",
-  "keyword1",
-  "keyword2",
-  "keyword3",
-  "quasi_keyword",
-  "improper",
-  "operator",
-  "tfree",
-  "tvar",
-  "free",
-  "skolem",
-  "bound",
-  "var",
-  "inner_numeral",
-  "inner_quoted",
-  "inner_cartouche",
-  "comment1",
-  "comment2",
-  "comment3",
-  "dynamic",
-  "class_parameter",
-  "antiquote",
-  "raw_text",
-  "plain_text"
+  'main',
+  'keyword1',
+  'keyword2',
+  'keyword3',
+  'quasi_keyword',
+  'improper',
+  'operator',
+  'tfree',
+  'tvar',
+  'free',
+  'skolem',
+  'bound',
+  'var',
+  'inner_numeral',
+  'inner_quoted',
+  'inner_cartouche',
+  'comment1',
+  'comment2',
+  'comment3',
+  'dynamic',
+  'class_parameter',
+  'antiquote',
+  'raw_text',
+  'plain_text'
 ]
 
 const text_overview_colors = [
-  "unprocessed",
-  "running",
-  "error",
-  "warning"
+  'unprocessed',
+  'running',
+  'error',
+  'warning'
 ]
 
 
@@ -132,21 +132,21 @@
   /* init */
 
   for (const color of background_colors) {
-    types.set("background_" + color, background(color))
+    types.set('background_' + color, background(color))
   }
   for (const color of foreground_colors) {
-    types.set("foreground_" + color, background(color)) // approximation
+    types.set('foreground_' + color, background(color)) // approximation
   }
   for (const color of dotted_colors) {
-    types.set("dotted_" + color, bottom_border("2px", "dotted", color))
+    types.set('dotted_' + color, bottom_border('2px', 'dotted', color))
   }
   for (const color of text_colors) {
-    types.set("text_" + color, text_color(color))
+    types.set('text_' + color, text_color(color))
   }
   for (const color of text_overview_colors) {
-    types.set("text_overview_" + color, text_overview_color(color))
+    types.set('text_overview_' + color, text_overview_color(color))
   }
-  types.set("spell_checker", bottom_border("1px", "solid", "spell_checker"))
+  types.set('spell_checker', bottom_border('1px', 'solid', 'spell_checker'))
 
 
   /* update editors */
@@ -160,23 +160,23 @@
 /* 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(decorations: DocumentDecorations)
+export function apply_decoration(decorations: Document_Decorations)
 {
-  const uri = IsabelleFSP.getIsabelleUri(decorations.uri);
+  const uri = Isabelle_FSP.get_isabelle(Uri.parse(decorations.uri))
 
-  for(const decoration of decorations.entries) {
+  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;
+          const r = opt.range
           return {
             range: new Range(r[0], r[1], r[2], r[3]),
             hoverMessage: opt.hover_message
@@ -188,7 +188,7 @@
       document_decorations.set(uri, document)
 
       for (const editor of window.visibleTextEditors) {
-        if (uri === editor.document.uri.toString()) {
+        if (uri.toString === editor.document.uri.toString) {
           editor.setDecorations(typ, content)
         }
       }
@@ -199,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)
@@ -222,7 +222,7 @@
       touched_editors.push(editor)
     }
   }
-  touched_documents.clear
+  touched_documents.clear()
   touched_editors.forEach(update_editor)
 }
 
--- a/src/Tools/VSCode/extension/src/extension.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,74 +1,74 @@
 'use strict';
 
-import * as path from 'path';
+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 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, ProgressLocation } from 'vscode';
-import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-languageclient';
-import { registerAbbreviations } from './abbreviations';
-import { IsabelleFSP } from './isabelle_filesystem/isabelleFSP';
-import { OutPutViewProvider } from './output_view';
-import { registerScriptDecorations } from './script_decorations';
+  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 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")
+  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")
+  if (isabelle_home === '')
+    window.showErrorMessage('Missing user settings: isabelle.home')
   else {
-    const discFolder = await IsabelleFSP.register(context);
-    const isabelle_tool = isabelle_home + "/bin/isabelle"
-    const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions", 
-    '-D', discFolder, '-d', discFolder
-      /* '-L', '/home/denis/Desktop/logi.log', '-v' */]
+    const workspace_dir = await Isabelle_FSP.register(context)
+    const roots = await workspace.findFiles('{ROOT,ROOTS}')
+    const isabelle_tool = isabelle_home + '/bin/isabelle'
+    const standard_args = ['-o', 'vscode_unicode_symbols', '-o', 'vscode_pide_extensions']
+    const session_args = roots.length > 0 ? ['-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) } :
+            (cygwin_root === '' ? path.join(isabelle_home, 'contrib', 'cygwin') : cygwin_root) +
+            '/bin/bash',
+          args: ['-l', isabelle_tool, 'vscode_server'].concat(standard_args, isabelle_args) } :
         { command: isabelle_tool,
-          args: ["vscode_server"].concat(standard_args, isabelle_args) };
-          
+          args: ['vscode_server'].concat(standard_args, isabelle_args, session_args) }
+
     const language_client_options: LanguageClientOptions = {
       documentSelector: [
-        /* { language: "isabelle", scheme: "file" }, */
-        { language: "isabelle", scheme: IsabelleFSP.scheme },
-        { language: "isabelle-ml", scheme: "file" },
-        { language: "bibtex", scheme: "file" }
+        { language: 'isabelle', scheme: Isabelle_FSP.scheme },
+        { language: 'isabelle-ml', scheme: 'file' },
+        { language: 'bibtex', scheme: 'file' }
       ],
       uriConverters: {
-        code2Protocol: uri => IsabelleFSP.getFileUri(uri.toString()),
-        protocol2Code: value => Uri.parse(IsabelleFSP.getIsabelleUri(value))
+        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)
+      new LanguageClient('Isabelle', server_options, language_client_options, false)
+
 
-    
-    window.withProgress({location: ProgressLocation.Notification, cancellable: false}, 
-      async (progress) => {
-        progress.report({
-          message: 'Waiting for Isabelle to start...'
-        });
-        return await language_client.onReady();
-    })
+    window.withProgress({location: ProgressLocation.Notification, cancellable: false},
+      async (progress) =>
+        {
+          progress.report({
+            message: 'Waiting for Isabelle server...'
+          })
+          await language_client.onReady()
+        })
+
 
     /* decorations */
 
@@ -85,8 +85,7 @@
 
     /* super-/subscript decorations */
 
-    registerScriptDecorations(context);
-
+    register_script_decorations(context)
 
 
     /* caret handling */
@@ -102,8 +101,8 @@
           caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character }
       }
       if (last_caret_update !== caret_update) {
-        if (caret_update.uri){
-          caret_update.uri = IsabelleFSP.getFileUri(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
@@ -119,7 +118,7 @@
       }
 
       if (caret_update.uri) {
-        caret_update.uri = IsabelleFSP.getIsabelleUri(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)
@@ -141,29 +140,22 @@
 
 
     /* dynamic output */
-    const provider = new OutPutViewProvider(context.extensionUri);
+
+    const provider = new Output_View_Provider(context.extensionUri)
     context.subscriptions.push(
-      window.registerWebviewViewProvider(OutPutViewProvider.viewType, provider));
-    // const dynamic_output = window.createOutputChannel("Isabelle Output")
-    // context.subscriptions.push(dynamic_output)
-    // dynamic_output.show(true)
-    // dynamic_output.hide()
+      window.registerWebviewViewProvider(Output_View_Provider.view_type, provider))
 
     language_client.onReady().then(() =>
     {
       language_client.onNotification(protocol.dynamic_output_type,
-        params => { 
-          provider.updateContent(params.content);
-          // dynamic_output.clear(); 
-          // dynamic_output.appendLine(params.content) 
-        })
+        params => provider.update_content(params.content))
     })
 
 
     /* state panel */
 
     context.subscriptions.push(
-      commands.registerCommand("isabelle.state", uri => state_panel.init(uri)))
+      commands.registerCommand('isabelle.state', uri => state_panel.init(uri)))
 
     language_client.onReady().then(() => state_panel.setup(context, language_client))
 
@@ -171,52 +163,33 @@
     /* preview panel */
 
     context.subscriptions.push(
-      commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)),
-      commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)))
+      commands.registerCommand('isabelle.preview', uri => preview_panel.request(uri, false)),
+      commands.registerCommand('isabelle.preview-split', uri => preview_panel.request(uri, true)))
 
     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,
-        ({entries}) => IsabelleFSP.initWorkspace(entries));
+        async ({entries}) => await Isabelle_FSP.init_workspace(entries))
 
       language_client.onNotification(protocol.symbols_type,
-        params => {
-          registerAbbreviations(params.entries, context);
-          IsabelleFSP.updateSymbolEncoder(params.entries);
-
-          //request theories to load in isabelle file system 
-          //after a valid symbol encoder is loaded
-          language_client.sendNotification(protocol.session_theories_request_type);
-        });
-
-      language_client.sendNotification(protocol.symbols_request_type);
-
-      //Reset system if changes to ROOT
-    })
+        params =>
+          {
+            //register_abbreviations(params.entries, context)
+            Isabelle_FSP.update_symbol_encoder(params.entries)
 
-    const watcher = workspace.createFileSystemWatcher({
-      base: discFolder,
-      pattern: '{ROOT,ROOTS}'
-    }, true, false, true);
-    watcher.onDidChange(() => 
-      language_client.sendNotification(
-        protocol.session_theories_request_type,
-        { reset: true}
-      ));
-    context.subscriptions.push(watcher)
+            // request theories to load in isabelle file system
+            // after a valid symbol encoder is loaded
+            language_client.sendNotification(protocol.session_theories_request_type)
+          })
 
-    /* completion */
+      language_client.sendNotification(protocol.symbols_request_type)
 
-    const completion_provider = new completion.Completion_Provider
-    for (const mode of ["isabelle", "isabelle-ml"]) {
-      context.subscriptions.push(
-        languages.registerCompletionItemProvider(mode, completion_provider))
-    }
+    })
 
 
     /* spell checker */
@@ -224,15 +197,15 @@
     language_client.onReady().then(() =>
     {
       context.subscriptions.push(
-        commands.registerCommand("isabelle.include-word", uri =>
+        commands.registerCommand('isabelle.include-word', uri =>
           language_client.sendNotification(protocol.include_word_type)),
-        commands.registerCommand("isabelle.include-word-permanently", uri =>
+        commands.registerCommand('isabelle.include-word-permanently', uri =>
           language_client.sendNotification(protocol.include_word_permanently_type)),
-        commands.registerCommand("isabelle.exclude-word", uri =>
+        commands.registerCommand('isabelle.exclude-word', uri =>
           language_client.sendNotification(protocol.exclude_word_type)),
-        commands.registerCommand("isabelle.exclude-word-permanently", uri =>
+        commands.registerCommand('isabelle.exclude-word-permanently', uri =>
           language_client.sendNotification(protocol.exclude_word_permanently_type)),
-        commands.registerCommand("isabelle.reset-words", uri =>
+        commands.registerCommand('isabelle.reset-words', uri =>
           language_client.sendNotification(protocol.reset_words_type)))
     })
 
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelleFSP.ts	Fri Sep 03 15:03:29 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,613 +0,0 @@
-import {
-    FileStat, FileType, FileSystemProvider, Uri, FileSystemError, FileChangeType,
-    FileChangeEvent, Event, Disposable, EventEmitter, ExtensionContext, workspace,
-    TextDocument, commands, window, ViewColumn, languages
-} from "vscode";
-import * as path from 'path';
-import { SymbolEncoder, SymbolEntry } from "./symbol_encoder";
-import { SessionTheories } from "../protocol";
-import { WorkspaceState, StateKey } from "./workspaceState";
-
-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 IsabelleFSP implements FileSystemProvider {
-
-    //#region Static Members
-    public static readonly scheme = 'isabelle';
-    private static symbolEncoder: SymbolEncoder;
-    private static instance: IsabelleFSP;
-    private static state: WorkspaceState;
-
-    public static async register(context: ExtensionContext): Promise<string> {
-        this.instance = new IsabelleFSP();
-        this.state = new WorkspaceState(context);
-        context.subscriptions.push(
-            workspace.registerFileSystemProvider(
-                this.scheme,
-                this.instance
-            ),
-
-            workspace.onDidOpenTextDocument((d) => {
-                this.instance.decideToCreate(d.uri, d.languageId);
-            }),
-
-            window.onDidChangeActiveTextEditor(async editor => {
-                if(!editor) return;
-
-                const { document } = editor;
-                if (document.uri.scheme === this.scheme) {
-                    this.instance.prepareTheory(document);
-                    return;
-                }
-
-                const newUri = await this.instance.decideToCreate(document.uri, document.languageId);
-
-                if (!newUri) return;
-                
-                const answer = await window.showInformationMessage(
-                    'Would you like to open the Isabelle theory associated with this file?',
-                    'Yes',
-                    'No'
-                )
-
-                if (answer !== 'Yes') {
-                    return;
-                }
-
-                await commands.executeCommand('workbench.action.closeActiveEditor');
-                await commands.executeCommand('vscode.open', Uri.parse(newUri), ViewColumn.Active);
-            }),
-
-            this.instance.syncFromOriginal(),
-
-            commands.registerCommand('isabelle.reload-workspace',
-                () => this.instance.reloadWorkspace()),
-
-            commands.registerTextEditorCommand(
-                'isabelle.reload-file',
-                (e) => {
-                    const fileUri = this.getFileUri(e.document.uri.toString());
-                    this.instance.reloadFile(Uri.parse(fileUri));
-                }
-            )
-        );
-
-        return await this.instance.setupWorkspace();
-    }
-
-    public static updateSymbolEncoder(entries: SymbolEntry[]) {
-        this.symbolEncoder = new SymbolEncoder(entries);
-        this.state.set(StateKey.symbolEntries, entries);
-    }
-
-    public static getFileUri(isabelleUri: string): string {
-        return this.instance.isabelleToFile.get(isabelleUri) || isabelleUri;
-    }
-
-    public static getIsabelleUri(fileUri: string): string {
-        return this.instance.fileToIsabelle.get(Uri.parse(fileUri).toString()) || fileUri;
-    }
-
-    public static initWorkspace(sessions: SessionTheories[]) {
-        this.instance.init(sessions);
-    }
-
-    //#endregion
-
-
-    private root = new Directory('');
-    private isabelleToFile = new Map<string, string>();
-    private fileToIsabelle = new Map<string, string>();
-    private sessionTheories: SessionTheories[] = [];
-
-
-    private async saveTreeState() {
-        const sessions: SessionTheories[] = [];
-        for(const [session_name, val] of this.root.entries){
-            if(!(val instanceof Directory)) return;
-            const theories: string[] = [];
-
-            for(const fileName of val.entries.keys()){
-                theories.push(
-                    this.isabelleToFile.get(
-                        Uri.parse(
-                            `${IsabelleFSP.scheme}:/${session_name}/${fileName}`
-                        ).toString()
-                    )
-                )
-            }
-
-            sessions.push({
-                session_name,
-                theories
-            });
-        }
-
-        IsabelleFSP.state.set(StateKey.sessions, sessions);
-    }
-
-
-    private async setupWorkspace(): Promise<string> {
-        const { state } = IsabelleFSP;
-        let { sessions, discFolder, symbolEntries} = state.getSetupData();
-        const mainFolderUri = Uri.parse(`${IsabelleFSP.scheme}:/`);
-
-        if(workspace.workspaceFolders[0].uri.toString() !== mainFolderUri.toString()){
-            workspace.updateWorkspaceFolders(0, 0,
-                {
-                    uri: mainFolderUri,
-                    name: "Isabelle - Theories"
-                }
-            );
-        }
-        
-        if(sessions && discFolder && symbolEntries){
-            IsabelleFSP.updateSymbolEncoder(symbolEntries);
-            await this.init(sessions);
-        } else {
-            discFolder = workspace.workspaceFolders[1].uri.fsPath;
-        }
-        
-        
-        state.set(StateKey.discFolder, discFolder);
-        this.saveTreeState();
-        this.onDidChangeFile(events => {
-            for(const e of events){
-                if(e.type === FileChangeType.Changed) continue;
-
-                this.saveTreeState();
-                return;
-            }
-        })
-        return discFolder;
-    }
-
-    private syncFromOriginal(): Disposable {
-        const watcher = workspace.createFileSystemWatcher("**/*.thy");
-        watcher.onDidChange(uri => this.reloadFile(uri));
-        watcher.onDidDelete(uri => {
-            const isabelleFile = this.fileToIsabelle.get(uri.toString());
-            if (!isabelleFile) {
-                return;
-            }
-            this._delete(Uri.parse(isabelleFile));
-        });
-        watcher.onDidCreate(uri => this.decideToCreate(uri, 'isabelle'));
-
-        return watcher;
-    }
-
-    private async prepareTheory(doc: TextDocument) {
-        if(doc.languageId !== 'isabelle')
-            languages.setTextDocumentLanguage(doc, 'isabelle');
-        
-        const uriString = doc.uri.toString();
-        const file = this.isabelleToFile.get(uriString);
-        if (!file) {
-            return;
-        }
-
-        const found = (await workspace.findFiles('**/*.thy'))
-            .find(uri => uri.toString() === file);
-        if (!found) {
-            window.showWarningMessage('Theory may or may not be synced with disc file!');
-        }
-    }
-
-    private syncDeletion(uri: Uri, silent: boolean) {
-        const dir = this._lookup(uri, silent);
-        if(!dir){
-            if(silent)
-                return;
-            else
-                throw FileSystemError.FileNotFound(uri);
-        }
-
-        const uriString = uri.toString();
-        if(dir instanceof Directory){
-            for(const key of dir.entries.keys()){
-                this.removeMapping(uriString + `/${key}`);
-            }
-        }
-        this.removeMapping(uriString);
-    }
-
-    private removeMapping(uri: string) {
-        const file = this.isabelleToFile.get(uri);
-        this.isabelleToFile.delete(uri);
-        this.fileToIsabelle.delete(file);
-    }
-
-    private async reloadFile(fileUri: Uri) {
-        const isabelleFile = this.fileToIsabelle.get(fileUri.toString());
-        if (!isabelleFile) {
-            return;
-        }
-
-        const data = await workspace.fs.readFile(fileUri);
-        const encodedData = IsabelleFSP.symbolEncoder.encode(data);
-        const isabelleUri = Uri.parse(isabelleFile);
-        this.writeFile(isabelleUri, encodedData, { create: false, overwrite: true });
-    }
-
-    private reloadWorkspace() {
-        this.init(this.sessionTheories);
-    }
-
-    private async init(sessions: SessionTheories[]) {
-        const sessionNames = sessions.map(s => s.session_name);
-        const rootEntries = Array.from(this.root.entries.keys());
-        for(const key of rootEntries){
-            if(key === 'Draft' || sessionNames.includes(key)) 
-                continue;
-
-            this._delete(Uri.parse(`${IsabelleFSP.scheme}:/${key}`), true);
-        }
-
-        for(const { session_name, theories } of sessions){
-            if(!session_name) continue;
-            if(session_name !== 'Draft') {
-                this.sessionTheories.push({
-                    session_name,
-                    theories: theories.map(t => Uri.parse(t).toString())
-                });
-            }
-
-            if(!rootEntries.includes(session_name)){
-                this._createDirectory(Uri.parse(`${IsabelleFSP.scheme}:/${session_name}`));
-            }
-        }
-
-        const promises = sessions.map(
-            ({ session_name, theories }) => theories.map(
-                async s => {
-                    try{
-                        if(session_name)
-                            return await this.createFromOriginal(Uri.parse(s), session_name);
-                        else 
-                            return Promise.resolve();
-                    } catch {
-                        return Promise.resolve();
-                    }
-                }
-            )
-        ).reduce((x, y) => x.concat(y), []);
-
-        await Promise.all(promises);
-    }
-
-    private createNewUri(uri: Uri, sessionName: string){
-        let newUri: Uri;
-        let extra = '';
-        let fsPath = uri.fsPath;
-        while(true){
-            const base = extra ? ` (${extra})` : '';
-            newUri = Uri.parse(
-                IsabelleFSP.scheme + ':' +
-                path.posix.join('/', sessionName, path.basename(uri.fsPath, '.thy') + base)
-            );
-
-            const oldUri = this.isabelleToFile.get(newUri.toString());
-            if(!oldUri || oldUri === uri.toString()) {
-                return newUri;
-            }
-
-            if(fsPath === '/') {
-                throw FileSystemError.FileExists(newUri);
-            }
-
-            fsPath = path.posix.dirname(fsPath);
-            extra = path.posix.join(path.posix.basename(fsPath), extra);
-        }
-    }
-
-    public async createFromOriginal(uri: Uri, sessionName: string): Promise<Uri> {
-        const data = await workspace.fs.readFile(uri);
-
-        const newUri = this.createNewUri(uri, sessionName);
-        const encodedData = IsabelleFSP.symbolEncoder.encode(data);
-
-        const isabelleFile = newUri.toString();
-        const discFile = uri.toString();
-        this.isabelleToFile.set(isabelleFile, discFile);
-        this.fileToIsabelle.set(discFile, isabelleFile);
-
-        await this.writeFile(newUri, encodedData, { create: true, overwrite: true });
-
-        return newUri;
-    }
-
-    public getTheorySession(uri: string): string {
-        let session = this.sessionTheories.find((s) => s.theories.includes(uri));
-        if (!session) {
-            if(!this.root.entries.get('Draft')){
-                this._createDirectory(Uri.parse(IsabelleFSP.scheme + ':/Draft'));
-            }
-            
-            return 'Draft';
-        }
-
-        return session.session_name;
-    }
-
-    public async decideToCreate(uri: Uri, languageId: string): Promise<string | undefined> {
-        if (
-            uri.scheme !== 'file' ||
-            languageId !== 'isabelle' ||
-            !IsabelleFSP.symbolEncoder
-        ) {
-            return;
-        }
-
-        const uriString = uri.toString();
-        const isabelleUri = this.fileToIsabelle.get(uriString);
-        if (isabelleUri) {
-            return isabelleUri;
-        }
-
-        const session = this.getTheorySession(uriString);
-        const createdUri = await this.createFromOriginal(uri, session);
-
-        return createdUri.toString();
-    }
-
-    private async syncOriginal(uri: Uri, content: Uint8Array) {
-        const originUri = Uri.parse(this.isabelleToFile.get(uri.toString()));
-        const decodedContent = IsabelleFSP.symbolEncoder.decode(content);
-        workspace.fs.writeFile(originUri, decodedContent);
-    }
-
-    stat(uri: Uri): FileStat {
-        return this._lookup(uri, false);
-    }
-
-    readDirectory(uri: Uri): [string, FileType][] {
-        const entry = this._lookupAsDirectory(uri, false);
-        const result: [string, FileType][] = [];
-        for (const [name, child] of entry.entries) {
-            result.push([name, child.type]);
-        }
-        return result;
-    }
-
-    // --- manage file contents
-
-    readFile(uri: Uri): Uint8Array {
-        const data = this._lookupAsFile(uri, false).data;
-        if (data) {
-            return data;
-        }
-        throw FileSystemError.FileNotFound();
-    }
-
-    async writeFile(uri: Uri, content: Uint8Array, options: { create: boolean, overwrite: boolean }): Promise<void> {
-        if (!IsabelleFSP.symbolEncoder) return;
-        if (!this.isabelleToFile.get(uri.toString())) {
-            throw FileSystemError.NoPermissions("No permission to create on Isabelle File System");
-        }
-
-        const basename = path.posix.basename(uri.path);
-        const [parent, parentUri] = this._getParentData(uri);
-        let entry = parent.entries.get(basename);
-        if (entry instanceof Directory) {
-            throw FileSystemError.FileIsADirectory(uri);
-        }
-        if (!entry && !options.create) {
-            throw FileSystemError.FileNotFound(uri);
-        }
-        if (entry && options.create && !options.overwrite) {
-            throw FileSystemError.FileExists(uri);
-        }
-
-        if (entry) {
-            if (options.create) {
-                this.syncOriginal(uri, content);
-                return;
-            }
-
-            entry.mtime = Date.now();
-            entry.size = content.byteLength;
-            entry.data = content;
-
-            this._fireSoon({ type: FileChangeType.Changed, 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._fireSoon(
-            { type: FileChangeType.Changed, uri: parentUri }, 
-            { type: FileChangeType.Created, uri }
-        );
-    }
-
-    // --- manage files/folders
-
-    rename(oldUri: Uri, newUri: Uri, options: { overwrite: boolean }): void {
-        throw FileSystemError.NoPermissions("No permission to rename on Isabelle File System");
-    }
-
-    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._lookupAsDirectory(dirname, silent);
-        
-        if(!parent) return;
-        if (!parent.entries.has(basename)) {
-            if(!silent)
-                throw FileSystemError.FileNotFound(uri);
-            else 
-                return;
-        }
-
-        this.syncDeletion(uri, silent);
-        parent.entries.delete(basename);
-        parent.mtime = Date.now();
-        parent.size -= 1;
-
-        this._fireSoon({ type: FileChangeType.Changed, uri: dirname }, { uri, type: FileChangeType.Deleted });
-    }
-
-    delete(uri: Uri): void {
-        const [parent, parentUri] = this._getParentData(uri)
-        if(parent && parent.name === 'Draft'){
-            if(parent.size === 1){
-                this._delete(parentUri);
-                return;
-            }
-
-            this._delete(uri);
-            return;
-        }
-
-        throw FileSystemError.NoPermissions("No permission to delete on Isabelle File System");
-        //In case it needs to be reactivated
-        this._delete(uri);
-    }
-
-    private _createDirectory(uri: Uri): void {
-        const basename = path.posix.basename(uri.path);
-        const [parent, parentUri] = this._getParentData(uri);
-
-        const entry = new Directory(basename);
-        parent.entries.set(entry.name, entry);
-        parent.mtime = Date.now();
-        parent.size += 1;
-        this._fireSoon(
-            { type: FileChangeType.Changed, uri: parentUri }, 
-            { type: FileChangeType.Created, uri }
-        );
-    }
-
-    createDirectory(uri: Uri): void {
-        throw FileSystemError.NoPermissions("No permission to create on Isabelle File System");
-        //In case it needs to be reactivated
-        this._createDirectory(uri);
-    }
-
-    private _getParentData(uri: Uri): [Directory, Uri] {
-        const parentUri = uri.with({ path: path.posix.dirname(uri.path) });
-        const parent = this._lookupAsDirectory(parentUri, false);
-
-        return [parent, parentUri];
-    }
-
-    // --- 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 _lookupAsDirectory(uri: Uri, silent: boolean): Directory {
-        const entry = this._lookup(uri, silent);
-        if (entry instanceof Directory) {
-            return entry;
-        }
-        throw FileSystemError.FileNotADirectory(uri);
-    }
-
-    private _lookupAsFile(uri: Uri, silent: boolean): File {
-        const entry = this._lookup(uri, silent);
-        if (entry instanceof File) {
-            return entry;
-        }
-        throw FileSystemError.FileIsADirectory(uri);
-    }
-
-    private _lookupParentDirectory(uri: Uri): Directory {
-        const dirname = uri.with({ path: path.posix.dirname(uri.path) });
-        return this._lookupAsDirectory(dirname, false);
-    }
-
-    // --- manage file events
-
-    private _emitter = new EventEmitter<FileChangeEvent[]>();
-    private _bufferedEvents: FileChangeEvent[] = [];
-    private _fireSoonHandle?: NodeJS.Timer;
-
-    readonly onDidChangeFile: Event<FileChangeEvent[]> = this._emitter.event;
-
-    watch(_resource: Uri): Disposable {
-        // ignore, fires for all changes...
-        return new Disposable(() => { });
-    }
-
-    private _fireSoon(...events: FileChangeEvent[]): void {
-        this._bufferedEvents.push(...events);
-
-        if (this._fireSoonHandle) {
-            clearTimeout(this._fireSoonHandle);
-        }
-
-        this._fireSoonHandle = setTimeout(() => {
-            this._emitter.fire(this._bufferedEvents);
-            this._bufferedEvents.length = 0;
-        }, 5);
-    }
-}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -0,0 +1,677 @@
+'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, Symbol_Entry} from './symbol_encoder';
+import {Session_Theories, session_theories_request_type} from '../protocol';
+import {State_Key, Workspace_State} from './workspace_state';
+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'
+
+  //#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>
+  {
+    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>
+  {
+    const { state } = Isabelle_FSP
+    let { sessions, workspace_dir, symbol_entries } = state.get_setup_data()
+    const main_folder_uri = Isabelle_FSP.get_dir_uri('')
+
+    if (workspace.workspaceFolders[0].uri.toString() !== main_folder_uri.toString()) {
+      workspace.updateWorkspaceFolders(0, 0,
+        {
+          uri: main_folder_uri,
+          name: 'Isabelle Sessions'
+        }
+      )
+    }
+
+    if (sessions && workspace_dir && symbol_entries) {
+      await Isabelle_FSP.update_symbol_encoder(symbol_entries)
+      await this.init_filesystem(sessions)
+    } else {
+      workspace_dir = workspace.workspaceFolders[1].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)
+  {
+    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)
+  {
+    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)
+  {
+    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)
+  {
+    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)
+  }
+}
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/prefix_tree.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/prefix_tree.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,82 +1,92 @@
-class TreeNode {
-    public key: number | string;
-    public parent: TreeNode = null;
-    public end: boolean = false;
-    public value: number[] | string;
-    public children: Record<number | string, TreeNode> = {};
-    constructor(key: number | string){
-        this.key = key;
-    }
+'use strict';
 
-    public getWord(): number[] | string[] {
-        let output = [];
-        let node: TreeNode = this;
-        
-        while (node.key !== null) {
-          output.unshift(node.key);
-          node = node.parent;
-        }
-        
-        return output;
-    }
-}
+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
+  }
 
-class PrefixTree {
-    private root: TreeNode;
+  public get_word(): number[] | string[]
+  {
+    let output = []
+    let node: Tree_Node = this
 
-    constructor(){
-        this.root = new TreeNode(null);
+    while (node.key !== null) {
+      output.unshift(node.key)
+      node = node.parent
     }
 
-    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 TreeNode(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 getNode(prefix: number[] | string): TreeNode | 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 getEndOrValue(prefix: number[] | string): TreeNode | undefined {
-        let node = this.root;
-        let resNode: TreeNode;
-        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;
-    }
+    return output
+  }
 }
 
-export { PrefixTree, TreeNode };
\ No newline at end of file
+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 }
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/symbol_encoder.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/symbol_encoder.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,7 +1,9 @@
-import { TextEncoder } from 'util';
-import { PrefixTree, TreeNode } from './prefix_tree';
+'use strict';
 
-export interface SymbolEntry
+import { TextEncoder } from 'util'
+import { Prefix_Tree, Tree_Node } from './prefix_tree'
+
+export interface Symbol_Entry
 {
   symbol: string,
   name: string,
@@ -9,78 +11,85 @@
   abbrevs: string[]
 }
 
-class EncodeData {
-    prefixTree: PrefixTree;
-    minLength: number;
-    maxLength: number;
+class Encode_Data
+{
+  prefix_tree: Prefix_Tree
+  min_length: number
+  max_length: number
 
-    constructor(origin: Uint8Array[], replacement: Uint8Array[]){
-        this.prefixTree = new PrefixTree();
+  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.minLength || this.minLength > entry.length)
-                this.minLength = entry.length;
-            
-            if(!this.maxLength || this.maxLength< entry.length)
-                this.maxLength = entry.length;
+    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
 
-            this.prefixTree.insert(Array.from(entry), Array.from(replacement[i]));
-        }
+      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 SymbolEncoder {
-    private symbols: EncodeData;
-    private sequences: EncodeData;
+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)
+  }
 
-    constructor(entries: SymbolEntry[]){
-        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)))
+  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
         }
-        this.symbols = new EncodeData(syms, seqs);
-        this.sequences = new EncodeData(seqs, syms);
+      }
+
+      if (node && node.end) {
+        result.push(...(node.value as number[]))
+        i += word.length - 1
+        continue
+      }
+      result.push(content[i])
     }
 
-    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: EncodeData, replacements: EncodeData): Uint8Array {
-        const result: number[] = [];
-
-        for(let i = 0; i < content.length; i++){
-            if(i > content.length - origin.minLength){
-                result.push(content[i]);
-                continue;
-            }
-
-            let word: number[] = [];
-            let node: TreeNode;
-            for(let j = i; j < i + origin.maxLength; j++){
-                word.push(content[j]);
-                node = origin.prefixTree.getNode(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);
-    }
-}
\ No newline at end of file
+    return new Uint8Array(result)
+  }
+}
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/workspaceState.ts	Fri Sep 03 15:03:29 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-import { ExtensionContext } from "vscode";
-import { SessionTheories } from "../protocol";
-import { SymbolEntry } from "./symbol_encoder";
-
-interface SetupData {
-    discFolder: string;
-    sessions: SessionTheories[];
-    symbolEntries: SymbolEntry[];
-}
-
-enum StateKey {
-    discFolder = 'discFolder',
-    sessions = 'sessions',
-    symbolEntries = "symbolEntries"
-}
-
-class WorkspaceState {
-    constructor(
-        private context: ExtensionContext
-    ) { }
-
-    public getSetupData(): SetupData {
-        return {
-            discFolder: this.get(StateKey.discFolder),
-            sessions: this.get<SessionTheories[]>(StateKey.sessions),
-            symbolEntries: this.get<SymbolEntry[]>(StateKey.symbolEntries)
-        }
-    }
-
-    public setSetupDate(setupData: SetupData) {
-        const {discFolder, sessions } = setupData;
-        this.set(StateKey.discFolder, discFolder);
-        this.set(StateKey.sessions, sessions)
-    }    
-
-    public get<T = string>(key: StateKey): T {
-        return this.context.workspaceState.get(key);
-    }
-
-    public async set(key: StateKey, value: any) {
-        await this.context.workspaceState.update(key, value);
-    }
-}
-
-export { WorkspaceState, StateKey, SetupData };
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -0,0 +1,52 @@
+'use strict';
+
+import { ExtensionContext } from 'vscode'
+import { Session_Theories } from '../protocol'
+import { Symbol_Entry as Symbol_Entry } from './symbol_encoder'
+
+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 }
--- a/src/Tools/VSCode/extension/src/library.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,23 +1,34 @@
 'use strict';
 
-import * as os from 'os';
-import { TextEditor, Uri, ViewColumn, workspace, window } from 'vscode'
-import { IsabelleFSP } from './isabelle_filesystem/isabelleFSP';
+import * as os from 'os'
+import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode'
+import {Isabelle_FSP} from './isabelle_filesystem/isabelle_fsp'
 
 
 /* regular expressions */
 
 export function escape_regex(s: string): string
 {
-  return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&")
+  return s.replace(/[|\\{}()[\]^$+*?.]/g, '\\$&')
 }
 
+/* strings */
+
+export function reverse(s: string): string
+{
+  return s.split('').reverse().join('')
+}
+
+export function has_newline(text: string)
+{
+  return text.includes('\n') || text.includes('\r')
+}
 
 /* platform information */
 
 export function platform_is_windows(): boolean
 {
-  return os.type().startsWith("Windows")
+  return os.type().startsWith('Windows')
 }
 
 
@@ -25,7 +36,7 @@
 
 export function is_file(uri: Uri): boolean
 {
-  return uri.scheme === "file" || uri.scheme === IsabelleFSP.scheme;
+  return uri.scheme === 'file' || uri.scheme === Isabelle_FSP.scheme
 }
 
 export function find_file_editor(uri: Uri): TextEditor | undefined
@@ -45,18 +56,23 @@
 
 export function get_configuration<T>(name: string): T
 {
-  return workspace.getConfiguration("isabelle").get<T>(name)
+  return workspace.getConfiguration('isabelle').get<T>(name)
 }
 
-export function get_replacement_mode() {
-  return get_configuration<'none' | 'non-alpha' | 'all'>('replacement');
+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 colors = get_configuration<object>("textColor");
-  const conf = colors[color + (light ? "_light" : "_dark")];
-  return conf;
+  const colors = get_configuration<object>('text_color')
+  return colors[color + (light ? '_light' : '_dark')]
 }
 
 
--- a/src/Tools/VSCode/extension/src/output_view.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/output_view.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,100 +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 { IsabelleFSP } from "./isabelle_filesystem/isabelleFSP";
+   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 OutPutViewProvider implements WebviewViewProvider {
-
-	public static readonly viewType = 'isabelle-output';
+class Output_View_Provider implements WebviewViewProvider
+{
 
-	private _view?: WebviewView;
-	private content: string = '';
+  public static readonly view_type = 'isabelle-output'
 
-	constructor(
-		private readonly _extensionUri: Uri,
-	) { }
+  private _view?: WebviewView
+  private content: string = ''
+
+  constructor(private readonly _extension_uri: Uri) { }
 
-	public resolveWebviewView(
-		webviewView: WebviewView,
-		context: WebviewViewResolveContext,
-		_token: CancellationToken,
-	) {
-		this._view = webviewView;
+  public resolveWebviewView(
+    view: WebviewView,
+    context: WebviewViewResolveContext,
+    _token: CancellationToken)
+  {
+    this._view = view
 
-		webviewView.webview.options = {
-			// Allow scripts in the webview
-			enableScripts: true,
+    view.webview.options = {
+      // Allow scripts in the webview
+      enableScripts: true,
 
-			localResourceRoots: [
-				this._extensionUri
-			]
-		};
+      localResourceRoots: [
+        this._extension_uri
+      ]
+    }
 
-		webviewView.webview.html = this._getHtml(this.content);
-		webviewView.webview.onDidReceiveMessage(async message => {
-			if (message.command === "open") {
-				webviewLinkOpen(message.link);
-			}
-		});
-	}
+    view.webview.html = this._get_html(this.content)
+    view.webview.onDidReceiveMessage(async message =>
+  {
+      if (message.command === 'open') {
+        open_webview_link(message.link)
+      }
+    })
+  }
 
-	public updateContent(content: string){
-		if(!this._view){
-			this.content = content;
-			return;
-		}
-		
-		this._view.webview.html = this._getHtml(content);
-	}
+  public update_content(content: string)
+  {
+    if (!this._view) {
+      this.content = content
+      return
+    }
 
-	private _getHtml(content: string): string {
-		return getHtmlForWebview(content, this._view.webview, this._extensionUri.fsPath);
-	}
+    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 webviewLinkOpen(link: string) {
-	const uri = Uri.parse(link);
-	const line = Number(uri.fragment) || 0;
-	const pos = new Position(line, 0);
-	const uriNoFragment = uri.with({ fragment: '' }).toString();
-	const isabelleUri = IsabelleFSP.getIsabelleUri(uriNoFragment);
-	window.showTextDocument(Uri.parse(isabelleUri), {
-		preserveFocus: false,
-		selection: new Selection(pos, pos)
-	});
+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 getHtmlForWebview(content: string, webview: Webview, extensionPath: string): string {
-	const scriptUri = webview.asWebviewUri(Uri.file(path.join(extensionPath, 'media', 'main.js')));
-	const styleVSCodeUri = webview.asWebviewUri(Uri.file(path.join(extensionPath, 'media', 'vscode.css')));
-	return `<!DOCTYPE html>
-		<html>
-			<head>
-				<meta charset="UTF-8">
-				<meta name="viewport" content="width=device-width, initial-scale=1.0">
-				<link href="${styleVSCodeUri}" rel="stylesheet" type="text/css">
-				<style>
-				${_getDecorations()}
-				</style>
-				<title>Output</title>
-			</head>
-			<body>
-				${content}
-				<script src="${scriptUri}"></script>
-			</body>
-		</html>`;
+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 _getDecorations(): 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`;
+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;
+  return style
 }
 
-export { OutPutViewProvider, getHtmlForWebview, webviewLinkOpen };
\ No newline at end of file
+export { Output_View_Provider, get_webview_html, open_webview_link }
--- a/src/Tools/VSCode/extension/src/preview_panel.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,8 +1,7 @@
 'use strict';
 
-import { ExtensionContext, Uri, workspace,
-  window, commands, ViewColumn, WebviewPanel } from 'vscode'
-import { LanguageClient } from 'vscode-languageclient';
+import { ExtensionContext, Uri, window, ViewColumn, WebviewPanel } from 'vscode'
+import { LanguageClient } from 'vscode-languageclient'
 import * as library from './library'
 import * as protocol from './protocol'
 
@@ -27,10 +26,10 @@
   constructor(column: ViewColumn)
   {
     this.webview_panel =
-      window.createWebviewPanel("isabelle-preview", "Preview", column,
+      window.createWebviewPanel('isabelle-preview', 'Preview', column,
         {
           enableScripts: true
-        });
+        })
     this.webview_panel.onDidDispose(() => { panel = null })
   }
 }
--- a/src/Tools/VSCode/extension/src/protocol.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/protocol.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,29 +1,29 @@
 'use strict';
 
 import { MarkdownString } from 'vscode'
-import { NotificationType } from 'vscode-languageclient';
-import { SymbolEntry } from './isabelle_filesystem/symbol_encoder';
+import { NotificationType } from 'vscode-languageclient'
+import { Symbol_Entry } from './isabelle_filesystem/symbol_encoder'
 
 /* decorations */
 
-export interface DecorationOpts {
+export interface Decoration_Options {
   range: number[],
   hover_message?: MarkdownString | MarkdownString[]
 }
 
 export interface Decoration
 {
-  "type": string;
-  content: DecorationOpts[];
+  'type': string
+  content: Decoration_Options[]
 }
 
-export interface DocumentDecorations {
-  uri: string;
+export interface Document_Decorations {
+  uri: string
   entries: Decoration[]
 }
 
 export const decoration_type =
-  new NotificationType<DocumentDecorations, void>("PIDE/decoration")
+  new NotificationType<Document_Decorations, void>('PIDE/decoration')
 
 
 /* caret handling */
@@ -37,7 +37,7 @@
 }
 
 export const caret_update_type =
-  new NotificationType<Caret_Update, void>("PIDE/caret_update")
+  new NotificationType<Caret_Update, void>('PIDE/caret_update')
 
 
 /* dynamic output */
@@ -48,20 +48,20 @@
 }
 
 export const dynamic_output_type =
-  new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")
+  new NotificationType<Dynamic_Output, void>('PIDE/dynamic_output')
 
 
 /* state */
 
 export interface State_Output
 {
-  id: number;
-  content: string;
-  auto_update: boolean;
+  id: number
+  content: string
+  auto_update: boolean
 }
 
 export const state_output_type =
-  new NotificationType<State_Output, void>("PIDE/state_output")
+  new NotificationType<State_Output, void>('PIDE/state_output')
 
 export interface State_Id
 {
@@ -74,12 +74,12 @@
   enabled: boolean
 }
 
-export const state_init_type = new NotificationType<void, void>("PIDE/state_init")
-export const state_exit_type = new NotificationType<State_Id, void>("PIDE/state_exit")
-export const state_locate_type = new NotificationType<State_Id, void>("PIDE/state_locate")
-export const state_update_type = new NotificationType<State_Id, void>("PIDE/state_update")
+export const state_init_type = new NotificationType<void, void>('PIDE/state_init')
+export const state_exit_type = new NotificationType<State_Id, void>('PIDE/state_exit')
+export const state_locate_type = new NotificationType<State_Id, void>('PIDE/state_locate')
+export const state_update_type = new NotificationType<State_Id, void>('PIDE/state_update')
 export const state_auto_update_type =
-  new NotificationType<Auto_Update, void>("PIDE/state_auto_update")
+  new NotificationType<Auto_Update, void>('PIDE/state_auto_update')
 
 
 /* preview */
@@ -99,52 +99,55 @@
 }
 
 export const preview_request_type =
-  new NotificationType<Preview_Request, void>("PIDE/preview_request")
+  new NotificationType<Preview_Request, void>('PIDE/preview_request')
 
 export const preview_response_type =
-  new NotificationType<Preview_Response, void>("PIDE/preview_response")
+  new NotificationType<Preview_Response, void>('PIDE/preview_response')
 
 
 /* Isabelle symbols */
 
 export interface Symbols
 {
-  entries: [SymbolEntry];
+  entries: [Symbol_Entry]
 }
 
 export const symbols_type =
-  new NotificationType<Symbols, void>("PIDE/symbols")
+  new NotificationType<Symbols, void>('PIDE/symbols')
 
 export const symbols_request_type =
-  new NotificationType<void, void>("PIDE/symbols_request")
+  new NotificationType<void, void>('PIDE/symbols_request')
 
-export interface Entries<T> {
-  entries: T[];
+export interface Entries<T>
+{
+  entries: T[]
 }
 
-export interface SessionTheories {
-  session_name: string;
+export interface Session_Theories
+{
+  session_name: string
   theories: string[]
 }
+
 export const session_theories_type =
-  new NotificationType<Entries<SessionTheories>, void>("PIDE/session_theories")
+  new NotificationType<Entries<Session_Theories>, void>('PIDE/session_theories')
 
 export const session_theories_request_type =
-  new NotificationType<void | { reset: boolean }, void>("PIDE/session_theories_request")
+  new NotificationType<void, void>('PIDE/session_theories_request')
 
 /* spell checker */
 
 export const include_word_type =
-  new NotificationType<void, void>("PIDE/include_word")
+  new NotificationType<void, void>('PIDE/include_word')
 
 export const include_word_permanently_type =
-  new NotificationType<void, void>("PIDE/include_word_permanently")
+  new NotificationType<void, void>('PIDE/include_word_permanently')
 
 export const exclude_word_type =
-  new NotificationType<void, void>("PIDE/exclude_word")
+  new NotificationType<void, void>('PIDE/exclude_word')
 
 export const exclude_word_permanently_type =
-  new NotificationType<void, void>("PIDE/exclude_word_permanently")
+  new NotificationType<void, void>('PIDE/exclude_word_permanently')
 
 export const reset_words_type =
-  new NotificationType<void, void>("PIDE/reset_words")
+  new NotificationType<void, void>('PIDE/reset_words')
--- a/src/Tools/VSCode/extension/src/script_decorations.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/script_decorations.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -1,125 +1,133 @@
-import { DecorationRangeBehavior, ExtensionContext, Range, 
-    TextDocument, TextEditor, window, workspace } from "vscode";
- 
+'use strict';
+
+import { DecorationRangeBehavior, ExtensionContext, Range,
+  TextDocument, TextEditor, window, workspace } from 'vscode'
+
 const arrows = {
-    sub: '⇩',
-    super: '⇧',
-    subBegin: '⇘',
-    subEnd: '⇙',
-    superBegin: '⇗',
-    superEnd: '⇖'
+  sub: '⇩',
+  sup: '⇧',
+  sub_begin: '⇘',
+  sub_end: '⇙',
+  sup_begin: '⇗',
+  sup_end: '⇖'
 }
-const noHideList = [' ', '\n', '\r', ...Object.values(arrows)];
+const no_hide_list = [' ', '\n', '\r', ...Object.values(arrows)]
 
-function shouldHide(nextChar: string): boolean{
-    return !noHideList.includes(nextChar);
+function should_hide(next_char: string): boolean
+{
+  return !no_hide_list.includes(next_char)
 }
 
-function findClosing(close: string, text: string, openIndex: number): number | undefined {
-    let closeIndex = openIndex;
-    let counter = 1;
-    const open = text[openIndex];
-    while (counter > 0) {
-        let c = text[++closeIndex];
-
-        if(c === undefined) return;
+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 === open) {
-            counter++;
-        }
-        else if (c === close) {
-            counter--;
-        }
+    if (c === undefined) return
+
+    if (c === open) {
+      counter++
     }
-    return closeIndex;
+    else if (c === close) {
+      counter--
+    }
+  }
+  return close_index
 }
 
 
 
-function extractRanges(doc: TextDocument) {
-    const text = doc.getText();
-    const hideRanges: Range[] = [];
-    const superscriptRanges: Range[] = [];
-    const subscriptRanges: Range[] = [];
+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.super:
-            case arrows.sub:
-                if(shouldHide(text[i + 1])){
-                    const posMid = doc.positionAt(i + 1);
-                    hideRanges.push(new Range(doc.positionAt(i), posMid));
-                    (text[i] === arrows.sub ? subscriptRanges : superscriptRanges)
-                        .push(new Range(posMid, doc.positionAt(i + 2)));
-                    i++;
-                }
-                break;
-            case arrows.superBegin:
-            case arrows.subBegin:
-                const close = text[i] === arrows.subBegin ? arrows.subEnd : arrows.superEnd;
-                const scriptRanges = text[i] === arrows.subBegin ? subscriptRanges : superscriptRanges;
-                const closeIndex = findClosing(close, text, i);
-                if(closeIndex && closeIndex - i > 1){
-                    const posStart = doc.positionAt(i + 1);
-                    const posEnd = doc.positionAt(closeIndex);
-                    hideRanges.push(
-                        new Range(doc.positionAt(i), posStart),
-                        new Range(posEnd, doc.positionAt(closeIndex + 1))
-                    );
-                    scriptRanges.push(new Range(posStart, posEnd));
-                    i = closeIndex;
-                }
-                break;
-            default:
-                break;
+  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)
 
-    return { hideRanges, superscriptRanges, subscriptRanges };
+        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 registerScriptDecorations(context: ExtensionContext){
-    const hide = window.createTextEditorDecorationType({
-      textDecoration: 'none; font-size: 0.001em',
-      rangeBehavior: DecorationRangeBehavior.ClosedClosed
-    });
+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; vertical-align: super; font-size: .83em'
-        textDecoration: 'none; position: relative; top: -0.5em; font-size: 80%'
-    });
+  const superscript = window.createTextEditorDecorationType({
+    textDecoration: 'none; position: relative; top: -0.5em; font-size: 80%'
+  })
 
-    const subscript = window.createTextEditorDecorationType({
-        //textDecoration: 'none; vertical-align: sub; font-size: .83em'
-        textDecoration: 'none; position: relative; bottom: -0.5em; font-size: 80%'
-    });
+  const subscript = window.createTextEditorDecorationType({
+    textDecoration: 'none; position: relative; bottom: -0.5em; font-size: 80%'
+  })
 
-    const setEditorDecs = (editor: TextEditor, doc: TextDocument) => {
-        const { hideRanges, superscriptRanges, subscriptRanges } = extractRanges(doc);
+  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);
+      editor.setDecorations(hide, hideRanges)
+      editor.setDecorations(superscript, superscriptRanges)
+      editor.setDecorations(subscript, subscriptRanges)
     }
 
-    context.subscriptions.push(
-        hide, superscript, subscript,
+  context.subscriptions.push(
+    hide, superscript, subscript,
 
-        window.onDidChangeActiveTextEditor(editor => {
-            if(!editor){
-                return;
-            }
+    window.onDidChangeActiveTextEditor(editor =>
+      {
+        if (!editor) {
+          return
+        }
 
-            const doc = editor.document;
-            setEditorDecs(editor, doc);
-        }),
-        
-        workspace.onDidChangeTextDocument(({document}) => {
-            for(const editor of window.visibleTextEditors){
-                if(editor.document.uri.toString() === document.uri.toString()){
-                    setEditorDecs(editor, document);
-                }
-            }
-        })
-    );
-}
\ No newline at end of file
+        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)
+          }
+        }
+      })
+  )
+}
--- a/src/Tools/VSCode/extension/src/state_panel.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/src/state_panel.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -2,11 +2,9 @@
 
 import * as library from './library'
 import * as protocol from './protocol'
-import * as path from 'path';
-import { LanguageClient } from 'vscode-languageclient';
-import { Uri, ExtensionContext, window, WebviewPanel, ViewColumn, Webview } from 'vscode'
-import { text_colors } from './decorations';
-import { getHtmlForWebview, webviewLinkOpen } from './output_view';
+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
@@ -20,15 +18,15 @@
 {
   private state_id: number
   private webview_panel: WebviewPanel
-  private _extensionPath: string
+  private _extension_path: string
 
   public get_id(): number { return this.state_id }
-  public check_id(id: number): boolean { return this.state_id == id }
+  public check_id(id: number): boolean { return this.state_id === id }
 
   public set_content(state: protocol.State_Output)
   {
     this.state_id = state.id
-    this.webview_panel.webview.html = this._getHtml(state.content, state.auto_update);
+    this.webview_panel.webview.html = this._get_html(state.content, state.auto_update)
   }
 
   public reveal()
@@ -36,50 +34,48 @@
     this.webview_panel.reveal(panel_column())
   }
 
-  constructor(extensionPath: string)
+  constructor(extension_path: string)
   {
-    this._extensionPath = extensionPath;
-    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;
-          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':
-            webviewLinkOpen(message.link);
-            break;
-          default:
-            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
+      }
+    })
   }
 
-  private _getHtml(content: string, auto_update: boolean): string {
-    const webview = this.webview_panel.webview;
+  private _get_html(content: string, auto_update: boolean): string
+  {
+    const webview = this.webview_panel.webview
     const checked = auto_update ? 'checked' : ''
-		const contentWithButtons = `<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>
+    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}`;
+    ${content}`
 
-    return getHtmlForWebview(contentWithButtons, webview, this._extensionPath);
-	}
+    return get_webview_html(content_with_buttons, webview, this._extension_path)
+  }
 }
 
 let panel: Panel
@@ -105,9 +101,9 @@
   language_client = client
   language_client.onNotification(protocol.state_output_type, params =>
     {
-      if (!panel) { 
-        panel = new Panel(context.extensionPath) 
+      if (!panel) {
+        panel = new Panel(context.extensionPath)
       }
       panel.set_content(params)
     })
-}
\ No newline at end of file
+}
--- a/src/Tools/VSCode/extension/test/index.ts	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/extension/test/index.ts	Wed Sep 08 16:53:16 2021 +0200
@@ -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
 });
 
--- a/src/Tools/VSCode/src/dynamic_output.scala	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Wed Sep 08 16:53:16 2021 +0200
@@ -35,26 +35,21 @@
             else this
         }
       if (st1.output != output) {
-        val elements3: Presentation.Elements =
-          Presentation.Elements(
-            html = Presentation.elements2.html,
-            language = Presentation.elements2.language,
-            entity = Markup.Elements.full)
+        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] =
-          (props, props) match {
-            case (Position.Def_File(thy_file), Position.Def_Line(def_line)) =>
-              val fileMaybe = resources.source_file(thy_file)
-              fileMaybe match {
-                  case Some(file) =>
-                    //val file = resources.node_file(value)
-                    Some(HTML.link(Path.explode(file).absolute_file.toURI.toString + "#" + def_line, body))
-                  case _ => None
-              }
-            case _ => None
-          }
+          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(
-          elements3,
+          elements,
           entity_link,
           Pretty.separate(st1.output))
 
--- a/src/Tools/VSCode/src/language_server.scala	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Sep 08 16:53:16 2021 +0200
@@ -51,7 +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
+    -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
@@ -77,9 +77,10 @@
         val log = Logger.make(log_file)
         val channel = new Channel(System.in, System.out, log, verbose)
         val server =
-          new Language_Server(channel, options, session_name = logic, session_dirs = dirs, select_dirs = select_dirs,
-            include_sessions = include_sessions, session_ancestor = logic_ancestor,
-            session_requirements = logic_requirements, modes = modes, log = log)
+          new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
+            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
@@ -102,9 +103,9 @@
   val channel: Channel,
   options: Options,
   session_name: String = Language_Server.default_logic,
+  include_sessions: List[String] = Nil,
   session_dirs: List[Path] = Nil,
   select_dirs: List[Path] = Nil,
-  include_sessions: List[String] = Nil,
   session_ancestor: Option[String] = None,
   session_requirements: Boolean = false,
   modes: List[String] = Nil,
@@ -118,20 +119,6 @@
   private val session_ = Synchronized(None: Option[Session])
   def session: Session = session_.value getOrElse error("Server inactive")
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
-  private var session_theories = Map[String, List[String]]();
-
-  def load_session_theories(): Unit = {
-    val sessions_structure = Sessions
-      .load_structure(Options.init(), select_dirs = select_dirs)
-      .selection(Sessions.Selection.empty)
-    val bases = Sessions.deps(sessions_structure).session_bases
-    session_theories = for {
-      (name, base) <- bases
-      sources = base
-        .session_theories
-        .map(_.path.absolute_file.toURI.toString)
-    } yield (name, sources)
-  }
 
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
@@ -231,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 =
@@ -281,17 +282,16 @@
 
     val try_session =
       try {
-        load_session_theories()
-
         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 + " ..."
@@ -375,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))
   }
 
@@ -486,12 +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(reset) => {
-            if(reset){
-              load_session_theories()
-            }
+          case LSP.Session_Theories_Request(()) =>
             channel.write(LSP.Session_Theories(session_theories))
-          }
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }
--- a/src/Tools/VSCode/src/lsp.scala	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Wed Sep 08 16:53:16 2021 +0200
@@ -160,7 +160,8 @@
         "textDocumentSync" -> 2,
         "completionProvider" -> JSON.Object(
           "resolveProvider" -> false,
-          "triggerCharacters" -> Symbol.abbrevs.map { _._2.split("") }.flatten.toSet.toList
+          "triggerCharacters" ->
+						Symbol.abbrevs.values.flatMap(_.iterator).map(_.toString).toList.distinct
         ),
         "hoverProvider" -> true,
         "definitionProvider" -> true,
@@ -509,15 +510,15 @@
       JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
   }
 
-  sealed case class Decoration(decos: List[(String, 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),
-          "entries" -> decos.map(c => JSON.Object(
-            "type" -> c._1,
-            "content" -> c._2.map(_.json))
+          "entries" -> decorations.map(decoration => JSON.Object(
+            "type" -> decoration._1,
+            "content" -> decoration._2.map(_.json))
           ))
       )
   }
@@ -643,25 +644,17 @@
     }
   }
 
-  object Session_Theories_Request {
-    def unapply(json: JSON.T): Option[Boolean] =
-      json match {
-        case Notification("PIDE/session_theories_request", Some(params)) => JSON.bool(params, "reset")
-        case Notification("PIDE/session_theories_request", None) => Option(false)
-        case _ => None
-      }
-  }
+  /* Session structure */
+
+  object Session_Theories_Request extends Notification0("PIDE/session_theories_request")
 
   object Session_Theories {
-    def apply(session_theories: Map[String, List[String]]): JSON.T = {
+    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
+        "theories" -> theories.map(Url.print_file)
       )}
-      Notification(
-        "PIDE/session_theories",
-        JSON.Object("entries" -> entries)
-      )
+      Notification("PIDE/session_theories", JSON.Object("entries" -> entries))
     }
   }
 }
--- a/src/Tools/VSCode/src/state_panel.scala	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Wed Sep 08 16:53:16 2021 +0200
@@ -61,35 +61,27 @@
 
   private val print_state =
     new Query_Operation(server.editor, (), "print_state", _ => (),
-      (snapshot, results, body) =>
-        if (output_active.value) {
-          if(body.nonEmpty){
-            val elements3: Presentation.Elements =
-              Presentation.Elements(
-                html = Presentation.elements2.html,
-                language = Presentation.elements2.language,
-                entity = Markup.Elements.full)
+      (_, _, 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] =
-              (props, props) match {
-                case (Position.Def_File(thy_file), Position.Def_Line(def_line)) =>
-                  val fileMaybe = server.resources.source_file(thy_file)
-                  fileMaybe match {
-                      case Some(file) =>
-                        //val file = resources.node_file(value)
-                        Some(HTML.link(Path.explode(file).absolute_file.toURI.toString + "#" + def_line, body))
-                      case _ => None
-                  }
-                case _ => None
-              }
+          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(
-              elements3,
-              entity_link,
-              Pretty.separate(body))
+          val htmlBody = Presentation.make_html(
+            elements,
+            entity_link,
+            Pretty.separate(body))
 
-            output(HTML.source(htmlBody).toString())
-          }
+          output(HTML.source(htmlBody).toString())
         })
 
   def locate(): Unit = print_state.locate_query()
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Sep 03 15:03:29 2021 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Sep 08 16:53:16 2021 +0200
@@ -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 = true, explicit = false,
+          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, true, syntax_completion.map(_.range), caret_range)
+            history, unicode, syntax_completion.map(_.range), caret_range)
 
         if (no_completion) Nil
         else {
@@ -121,7 +122,7 @@
               case Some(result) =>
                 result.items.map(item =>
                   LSP.CompletionItem(
-                    label = (Some(item.description.mkString(" ")) getOrElse(item.replacement)) + " " + item.original ,
+                    label = item.description.mkString(" "),
                     text = Some(item.replacement),
                     range = Some(doc.range(item.range))))
             }
@@ -238,12 +239,12 @@
   {
     val entries = for(deco <- decoration)
         yield {
-          val decopts = (for(Text.Info(text_range, msgs) <- deco.content)
+          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)
         }