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