--- a/src/Tools/VSCode/extension/.vscode/tasks.json Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/extension/.vscode/tasks.json Fri Sep 03 15:03:29 2021 +0200
@@ -8,17 +8,11 @@
// A task runner that calls a custom npm script that compiles the extension.
{
- "version": "0.1.0",
+ "version": "2.0.0",
// we want to run npm
"command": "npm",
- // the command is a shell script
- "isShellCommand": true,
-
- // show the output window only if unrecognized errors occur.
- "showOutput": "silent",
-
// we run the custom script "compile" as defined in package.json
"args": ["run", "compile", "--loglevel", "silent"],
@@ -26,5 +20,21 @@
"isWatching": true,
// use the standard tsc in watch mode problem matcher to find compile problems in the output.
- "problemMatcher": "$tsc-watch"
+ "problemMatcher": "$tsc-watch",
+ "tasks": [
+ {
+ "label": "npm",
+ "type": "shell",
+ "command": "npm",
+ "args": [
+ "run",
+ "compile",
+ "--loglevel",
+ "silent"
+ ],
+ "isBackground": true,
+ "problemMatcher": "$tsc-watch",
+ "group": "build"
+ }
+ ]
}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/main.js Fri Sep 03 15:03:29 2021 +0200
@@ -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 Fri Sep 03 15:03:29 2021 +0200
@@ -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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/package-lock.json Fri Sep 03 15:03:29 2021 +0200
@@ -0,0 +1,377 @@
+{
+ "name": "Isabelle",
+ "version": "1.2.2",
+ "lockfileVersion": 1,
+ "requires": true,
+ "dependencies": {
+ "@types/mocha": {
+ "version": "2.2.48",
+ "resolved": "https://registry.npmjs.org/@types/mocha/-/mocha-2.2.48.tgz",
+ "integrity": "sha512-nlK/iyETgafGli8Zh9zJVCTicvU3iajSkRwOh3Hhiva598CMqNJ4NcVCGMTGKpGpTYj/9R8RLzS9NAykSSCqGw==",
+ "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==",
+ "dev": true
+ },
+ "@types/vscode": {
+ "version": "1.55.0",
+ "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.55.0.tgz",
+ "integrity": "sha512-49hysH7jneTQoSC8TWbAi7nKK9Lc5osQNjmDHVosrcU8o3jecD9GrK0Qyul8q4aGPSXRfNGqIp9CBdb13akETg=="
+ },
+ "balanced-match": {
+ "version": "1.0.0",
+ "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.0.tgz",
+ "integrity": "sha1-ibTRmasr7kneFk6gK4nORi1xt2c=",
+ "dev": true
+ },
+ "brace-expansion": {
+ "version": "1.1.11",
+ "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.11.tgz",
+ "integrity": "sha512-iCuPHDFgrHX7H2vEI/5xpz07zSHB00TpugqhmYtVmMO6518mCuRMoOYFldEBl0g187ufozdaHgWKcYFb61qGiA==",
+ "dev": true,
+ "requires": {
+ "balanced-match": "^1.0.0",
+ "concat-map": "0.0.1"
+ }
+ },
+ "browser-stdout": {
+ "version": "1.3.0",
+ "resolved": "https://registry.npmjs.org/browser-stdout/-/browser-stdout-1.3.0.tgz",
+ "integrity": "sha1-81HTKWnTL6XXpVZxVCY9korjvR8=",
+ "dev": true
+ },
+ "commander": {
+ "version": "2.9.0",
+ "resolved": "https://registry.npmjs.org/commander/-/commander-2.9.0.tgz",
+ "integrity": "sha1-nJkJQXbhIkDLItbFFGCYQA/g99Q=",
+ "dev": true,
+ "requires": {
+ "graceful-readlink": ">= 1.0.0"
+ }
+ },
+ "concat-map": {
+ "version": "0.0.1",
+ "resolved": "https://registry.npmjs.org/concat-map/-/concat-map-0.0.1.tgz",
+ "integrity": "sha1-2Klr13/Wjfd5OnMDajug1UBdR3s=",
+ "dev": true
+ },
+ "debug": {
+ "version": "2.6.8",
+ "resolved": "https://registry.npmjs.org/debug/-/debug-2.6.8.tgz",
+ "integrity": "sha1-5zFTHKLt4n0YgiJCfaF4IdaP9Pw=",
+ "dev": true,
+ "requires": {
+ "ms": "2.0.0"
+ }
+ },
+ "diff": {
+ "version": "3.2.0",
+ "resolved": "https://registry.npmjs.org/diff/-/diff-3.2.0.tgz",
+ "integrity": "sha1-yc45Okt8vQsFinJck98pkCeGj/k=",
+ "dev": true
+ },
+ "escape-string-regexp": {
+ "version": "1.0.5",
+ "resolved": "https://registry.npmjs.org/escape-string-regexp/-/escape-string-regexp-1.0.5.tgz",
+ "integrity": "sha1-G2HAViGQqN/2rjuyzwIAyhMLhtQ=",
+ "dev": true
+ },
+ "fs.realpath": {
+ "version": "1.0.0",
+ "resolved": "https://registry.npmjs.org/fs.realpath/-/fs.realpath-1.0.0.tgz",
+ "integrity": "sha1-FQStJSMVjKpA20onh8sBQRmU6k8=",
+ "dev": true
+ },
+ "glob": {
+ "version": "7.1.1",
+ "resolved": "https://registry.npmjs.org/glob/-/glob-7.1.1.tgz",
+ "integrity": "sha1-gFIR3wT6rxxjo2ADBs31reULLsg=",
+ "dev": true,
+ "requires": {
+ "fs.realpath": "^1.0.0",
+ "inflight": "^1.0.4",
+ "inherits": "2",
+ "minimatch": "^3.0.2",
+ "once": "^1.3.0",
+ "path-is-absolute": "^1.0.0"
+ }
+ },
+ "graceful-readlink": {
+ "version": "1.0.1",
+ "resolved": "https://registry.npmjs.org/graceful-readlink/-/graceful-readlink-1.0.1.tgz",
+ "integrity": "sha1-TK+tdrxi8C+gObL5Tpo906ORpyU=",
+ "dev": true
+ },
+ "growl": {
+ "version": "1.9.2",
+ "resolved": "https://registry.npmjs.org/growl/-/growl-1.9.2.tgz",
+ "integrity": "sha1-Dqd0NxXbjY3ixe3hd14bRayFwC8=",
+ "dev": true
+ },
+ "has-flag": {
+ "version": "1.0.0",
+ "resolved": "https://registry.npmjs.org/has-flag/-/has-flag-1.0.0.tgz",
+ "integrity": "sha1-nZ55MWXOAXoA8AQYxD+UKnsdEfo=",
+ "dev": true
+ },
+ "he": {
+ "version": "1.1.1",
+ "resolved": "https://registry.npmjs.org/he/-/he-1.1.1.tgz",
+ "integrity": "sha1-k0EP0hsAlzUVH4howvJx80J+I/0=",
+ "dev": true
+ },
+ "inflight": {
+ "version": "1.0.6",
+ "resolved": "https://registry.npmjs.org/inflight/-/inflight-1.0.6.tgz",
+ "integrity": "sha1-Sb1jMdfQLQwJvJEKEHW6gWW1bfk=",
+ "dev": true,
+ "requires": {
+ "once": "^1.3.0",
+ "wrappy": "1"
+ }
+ },
+ "inherits": {
+ "version": "2.0.4",
+ "resolved": "https://registry.npmjs.org/inherits/-/inherits-2.0.4.tgz",
+ "integrity": "sha512-k/vGaX4/Yla3WzyMCvTQOXYeIHvqOKtnqBduzTHpzpQZzAskKMhZ2K+EnBiSM9zGSoIFeMpXKxa4dYeZIQqewQ==",
+ "dev": true
+ },
+ "json3": {
+ "version": "3.3.2",
+ "resolved": "https://registry.npmjs.org/json3/-/json3-3.3.2.tgz",
+ "integrity": "sha1-PAQ0dD35Pi9cQq7nsZvLSDV19OE=",
+ "dev": true
+ },
+ "lodash._baseassign": {
+ "version": "3.2.0",
+ "resolved": "https://registry.npmjs.org/lodash._baseassign/-/lodash._baseassign-3.2.0.tgz",
+ "integrity": "sha1-jDigmVAPIVrQnlnxci/QxSv+Ck4=",
+ "dev": true,
+ "requires": {
+ "lodash._basecopy": "^3.0.0",
+ "lodash.keys": "^3.0.0"
+ }
+ },
+ "lodash._basecopy": {
+ "version": "3.0.1",
+ "resolved": "https://registry.npmjs.org/lodash._basecopy/-/lodash._basecopy-3.0.1.tgz",
+ "integrity": "sha1-jaDmqHbPNEwK2KVIghEd08XHyjY=",
+ "dev": true
+ },
+ "lodash._basecreate": {
+ "version": "3.0.3",
+ "resolved": "https://registry.npmjs.org/lodash._basecreate/-/lodash._basecreate-3.0.3.tgz",
+ "integrity": "sha1-G8ZhYU2qf8MRt9A78WgGoCE8+CE=",
+ "dev": true
+ },
+ "lodash._getnative": {
+ "version": "3.9.1",
+ "resolved": "https://registry.npmjs.org/lodash._getnative/-/lodash._getnative-3.9.1.tgz",
+ "integrity": "sha1-VwvH3t5G1hzc3mh9ZdPuy6o6r/U=",
+ "dev": true
+ },
+ "lodash._isiterateecall": {
+ "version": "3.0.9",
+ "resolved": "https://registry.npmjs.org/lodash._isiterateecall/-/lodash._isiterateecall-3.0.9.tgz",
+ "integrity": "sha1-UgOte6Ql+uhCRg5pbbnPPmqsBXw=",
+ "dev": true
+ },
+ "lodash.create": {
+ "version": "3.1.1",
+ "resolved": "https://registry.npmjs.org/lodash.create/-/lodash.create-3.1.1.tgz",
+ "integrity": "sha1-1/KEnw29p+BGgruM1yqwIkYd6+c=",
+ "dev": true,
+ "requires": {
+ "lodash._baseassign": "^3.0.0",
+ "lodash._basecreate": "^3.0.0",
+ "lodash._isiterateecall": "^3.0.0"
+ }
+ },
+ "lodash.isarguments": {
+ "version": "3.1.0",
+ "resolved": "https://registry.npmjs.org/lodash.isarguments/-/lodash.isarguments-3.1.0.tgz",
+ "integrity": "sha1-L1c9hcaiQon/AGY7SRwdM4/zRYo=",
+ "dev": true
+ },
+ "lodash.isarray": {
+ "version": "3.0.4",
+ "resolved": "https://registry.npmjs.org/lodash.isarray/-/lodash.isarray-3.0.4.tgz",
+ "integrity": "sha1-eeTriMNqgSKvhvhEqpvNhRtfu1U=",
+ "dev": true
+ },
+ "lodash.keys": {
+ "version": "3.1.2",
+ "resolved": "https://registry.npmjs.org/lodash.keys/-/lodash.keys-3.1.2.tgz",
+ "integrity": "sha1-TbwEcrFWvlCgsoaFXRvQsMZWCYo=",
+ "dev": true,
+ "requires": {
+ "lodash._getnative": "^3.0.0",
+ "lodash.isarguments": "^3.0.0",
+ "lodash.isarray": "^3.0.0"
+ }
+ },
+ "minimatch": {
+ "version": "3.0.4",
+ "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-3.0.4.tgz",
+ "integrity": "sha512-yJHVQEhyqPLUTgt9B83PXu6W3rx4MvvHvSUvToogpwoGDOUQ+yDrR0HRot+yOCdCO7u4hX3pWft6kWBBcqh0UA==",
+ "dev": true,
+ "requires": {
+ "brace-expansion": "^1.1.7"
+ }
+ },
+ "minimist": {
+ "version": "0.0.8",
+ "resolved": "https://registry.npmjs.org/minimist/-/minimist-0.0.8.tgz",
+ "integrity": "sha1-hX/Kv8M5fSYluCKCYuhqp6ARsF0=",
+ "dev": true
+ },
+ "mkdirp": {
+ "version": "0.5.1",
+ "resolved": "https://registry.npmjs.org/mkdirp/-/mkdirp-0.5.1.tgz",
+ "integrity": "sha1-MAV0OOrGz3+MR2fzhkjWaX11yQM=",
+ "dev": true,
+ "requires": {
+ "minimist": "0.0.8"
+ }
+ },
+ "mocha": {
+ "version": "3.5.3",
+ "resolved": "https://registry.npmjs.org/mocha/-/mocha-3.5.3.tgz",
+ "integrity": "sha512-/6na001MJWEtYxHOV1WLfsmR4YIynkUEhBwzsb+fk2qmQ3iqsi258l/Q2MWHJMImAcNpZ8DEdYAK72NHoIQ9Eg==",
+ "dev": true,
+ "requires": {
+ "browser-stdout": "1.3.0",
+ "commander": "2.9.0",
+ "debug": "2.6.8",
+ "diff": "3.2.0",
+ "escape-string-regexp": "1.0.5",
+ "glob": "7.1.1",
+ "growl": "1.9.2",
+ "he": "1.1.1",
+ "json3": "3.3.2",
+ "lodash.create": "3.1.1",
+ "mkdirp": "0.5.1",
+ "supports-color": "3.1.2"
+ }
+ },
+ "ms": {
+ "version": "2.0.0",
+ "resolved": "https://registry.npmjs.org/ms/-/ms-2.0.0.tgz",
+ "integrity": "sha1-VgiurfwAvmwpAd9fmGF4jeDVl8g=",
+ "dev": true
+ },
+ "once": {
+ "version": "1.4.0",
+ "resolved": "https://registry.npmjs.org/once/-/once-1.4.0.tgz",
+ "integrity": "sha1-WDsap3WWHUsROsF9nFC6753Xa9E=",
+ "dev": true,
+ "requires": {
+ "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",
+ "integrity": "sha512-sauaDf/PZdVgrLTNYHRtpXa1iRiKcaebiKQ1BJdpQlWH2lCvexQdX55snPFyK7QzpudqbCI0qXFfOasHdyNDGQ=="
+ },
+ "supports-color": {
+ "version": "3.1.2",
+ "resolved": "https://registry.npmjs.org/supports-color/-/supports-color-3.1.2.tgz",
+ "integrity": "sha1-cqJiiU2dQIuVbKBf83su2KbiotU=",
+ "dev": true,
+ "requires": {
+ "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==",
+ "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",
+ "integrity": "sha512-perEnXQdQOJMTDFNv+UF3h1Y0z4iSiaN9jIlb0OqIYgosPCZGYh/MCUlkFtV2668PL69lRDO32hmvL2yiidUYg=="
+ },
+ "vscode-languageclient": {
+ "version": "5.2.1",
+ "resolved": "https://registry.npmjs.org/vscode-languageclient/-/vscode-languageclient-5.2.1.tgz",
+ "integrity": "sha512-7jrS/9WnV0ruqPamN1nE7qCxn0phkH5LjSgSp9h6qoJGoeAKzwKz/PF6M+iGA/aklx4GLZg1prddhEPQtuXI1Q==",
+ "requires": {
+ "semver": "^5.5.0",
+ "vscode-languageserver-protocol": "3.14.1"
+ }
+ },
+ "vscode-languageserver-protocol": {
+ "version": "3.14.1",
+ "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.14.1.tgz",
+ "integrity": "sha512-IL66BLb2g20uIKog5Y2dQ0IiigW0XKrvmWiOvc0yXw80z3tMEzEnHjaGAb3ENuU7MnQqgnYJ1Cl2l9RvNgDi4g==",
+ "requires": {
+ "vscode-jsonrpc": "^4.0.0",
+ "vscode-languageserver-types": "3.14.0"
+ },
+ "dependencies": {
+ "vscode-languageserver-types": {
+ "version": "3.14.0",
+ "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.14.0.tgz",
+ "integrity": "sha512-lTmS6AlAlMHOvPQemVwo3CezxBp0sNB95KNPkqp3Nxd5VFEnuG1ByM0zlRWos0zjO3ZWtkvhal0COgiV1xIA4A=="
+ }
+ }
+ },
+ "vscode-languageserver-types": {
+ "version": "3.16.0",
+ "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.16.0.tgz",
+ "integrity": "sha512-k8luDIWJWyenLc5ToFQQMaSrqCHiLwyKPHKPQZ5zz21vM+vIVUSvsRpcbiECH4WR88K2XZqc4ScRcZ7nk/jbeA=="
+ },
+ "wrappy": {
+ "version": "1.0.2",
+ "resolved": "https://registry.npmjs.org/wrappy/-/wrappy-1.0.2.tgz",
+ "integrity": "sha1-tSQ9jz7BqjXxNkYFvA0QNuMKtp8=",
+ "dev": true
+ }
+ }
+}
--- a/src/Tools/VSCode/extension/package.json Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/extension/package.json Fri Sep 03 15:03:29 2021 +0200
@@ -1,5 +1,5 @@
{
- "name": "Isabelle",
+ "name": "isabelle-vscode",
"displayName": "Isabelle",
"description": "Isabelle Prover IDE",
"keywords": [
@@ -23,16 +23,42 @@
"Programming Languages"
],
"activationEvents": [
- "onLanguage:isabelle",
- "onLanguage:isabelle-ml",
- "onLanguage:bibtex",
- "onCommand:isabelle.preview",
- "onCommand:isabelle.preview-split"
+ "workspaceContains:ROOT",
+ "workspaceContains:ROOTS",
+ "onFileSystem:isabelle"
],
"main": "./out/src/extension",
"contributes": {
+ "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"
+ },
+ {
"command": "isabelle.state",
"title": "Show State",
"category": "Isabelle"
@@ -189,349 +215,110 @@
"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)"
- },
- "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)"
+ "default": "non-alpha",
+ "enum": ["none", "non-alpha", "all"],
+ "enumDescriptions": [
+ "Replacments are deactivated. No replacments are done.",
+ "Replaces all uniqe abbreviations that contain no alpha numeric characters",
+ "Replaces all uniqe abbreviations"
+ ],
+ "description": "Aggressive replacement mode"
},
- "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.textColor":{
+ "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)"
+ }
}
}
}
@@ -545,10 +332,12 @@
"@types/mocha": "^2.2.48",
"@types/node": "^10.11.0",
"mocha": "^3.5.3",
- "typescript": "^3.9.9",
- "vscode": "^1.1.36"
+ "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"
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/abbreviations.ts Fri Sep 03 15:03:29 2021 +0200
@@ -0,0 +1,146 @@
+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";
+
+const entries: Record<string, string> = {};
+const prefixTree: PrefixTree = new PrefixTree();
+
+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();
+
+ 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;
+ }
+
+ const beginOffset = endOffset < maxLength ? 0 : endOffset - maxLength;
+
+ 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 word = node.getWord().join('');
+ if(mode == 'non-alpha' && !regEx.test(word)){
+ continue;
+ }
+
+ beginPos = doc.positionAt(endOffset - word.length);
+ range = new Range(beginPos, endPos);
+
+ edits.replace(doc.uri, range, node.value as string);
+ }
+
+ applyEdits(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');
+}
+
+function waitForNextTick(): Promise<void> {
+ return new Promise((res) => setTimeout(res, 0));
+}
+
+export { registerAbbreviations };
\ No newline at end of file
--- a/src/Tools/VSCode/extension/src/completion.ts Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/extension/src/completion.ts Fri Sep 03 15:03:29 2021 +0200
@@ -1,6 +1,5 @@
'use strict';
-import * as symbol from './symbol'
import { CompletionItemProvider, CompletionItem, TextDocument, Range, Position,
CancellationToken, CompletionList } from 'vscode'
--- a/src/Tools/VSCode/extension/src/decorations.ts Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts Fri Sep 03 15:03:29 2021 +0200
@@ -2,10 +2,11 @@
import * as timers from 'timers'
import { window, OverviewRulerLane } from 'vscode'
-import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
+import { Range, DecorationOptions, DecorationRenderOptions,
TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
-import { Decoration } from './protocol'
+import { DocumentDecorations } from './protocol'
import * as library from './library'
+import { IsabelleFSP } from './isabelle_filesystem/isabelleFSP';
/* known decoration types */
@@ -35,7 +36,7 @@
"warning"
]
-const text_colors = [
+export const text_colors = [
"main",
"keyword1",
"keyword2",
@@ -166,27 +167,30 @@
document_decorations.delete(document.uri.toString())
}
-export function apply_decoration(decoration: Decoration)
+export function apply_decoration(decorations: DocumentDecorations)
{
- 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 = IsabelleFSP.getIsabelleUri(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 === 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)
}
}
}
--- a/src/Tools/VSCode/extension/src/extension.ts Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Fri Sep 03 15:03:29 2021 +0200
@@ -1,23 +1,24 @@
'use strict';
import * as path from 'path';
-import * as fs from 'fs';
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 { Uri, TextEditor, ViewColumn, Selection, Position, ExtensionContext, workspace, window,
- commands, languages } from 'vscode';
-import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind,
- NotificationType } from 'vscode-languageclient';
+ 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';
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 +30,11 @@
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"]
+ const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions",
+ '-D', discFolder, '-d', discFolder
+ /* '-L', '/home/denis/Desktop/logi.log', '-v' */]
const server_options: ServerOptions =
library.platform_is_windows() ?
@@ -40,17 +44,31 @@
args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } :
{ command: isabelle_tool,
args: ["vscode_server"].concat(standard_args, isabelle_args) };
+
const language_client_options: LanguageClientOptions = {
documentSelector: [
- { language: "isabelle", scheme: "file" },
+ /* { language: "isabelle", scheme: "file" }, */
+ { language: "isabelle", scheme: IsabelleFSP.scheme },
{ language: "isabelle-ml", scheme: "file" },
{ language: "bibtex", scheme: "file" }
- ]
+ ],
+ uriConverters: {
+ code2Protocol: uri => IsabelleFSP.getFileUri(uri.toString()),
+ protocol2Code: value => Uri.parse(IsabelleFSP.getIsabelleUri(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 to start...'
+ });
+ return await language_client.onReady();
+ })
/* decorations */
@@ -65,6 +83,12 @@
language_client.onNotification(protocol.decoration_type, decorations.apply_decoration))
+ /* super-/subscript decorations */
+
+ registerScriptDecorations(context);
+
+
+
/* caret handling */
function update_caret()
@@ -78,8 +102,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 = IsabelleFSP.getFileUri(caret_update.uri);
language_client.sendNotification(protocol.caret_update_type, caret_update)
+ }
last_caret_update = caret_update
}
}
@@ -93,6 +119,7 @@
}
if (caret_update.uri) {
+ caret_update.uri = IsabelleFSP.getIsabelleUri(caret_update.uri);
workspace.openTextDocument(Uri.parse(caret_update.uri)).then(document =>
{
const editor = library.find_file_editor(document.uri)
@@ -114,16 +141,22 @@
/* dynamic output */
-
- const dynamic_output = window.createOutputChannel("Isabelle Output")
- context.subscriptions.push(dynamic_output)
- dynamic_output.show(true)
- dynamic_output.hide()
+ const provider = new OutPutViewProvider(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()
language_client.onReady().then(() =>
{
language_client.onNotification(protocol.dynamic_output_type,
- params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) })
+ params => {
+ provider.updateContent(params.content);
+ // dynamic_output.clear();
+ // dynamic_output.appendLine(params.content)
+ })
})
@@ -148,11 +181,34 @@
language_client.onReady().then(() =>
{
+ language_client.onNotification(protocol.session_theories_type,
+ ({entries}) => IsabelleFSP.initWorkspace(entries));
+
language_client.onNotification(protocol.symbols_type,
- params => symbol.setup(context, params.entries))
- language_client.sendNotification(protocol.symbols_request_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
})
+ 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)
/* completion */
@@ -187,4 +243,5 @@
}
}
+
export function deactivate() { }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelleFSP.ts Fri Sep 03 15:03:29 2021 +0200
@@ -0,0 +1,613 @@
+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/prefix_tree.ts Fri Sep 03 15:03:29 2021 +0200
@@ -0,0 +1,82 @@
+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;
+ }
+
+ public getWord(): number[] | string[] {
+ let output = [];
+ let node: TreeNode = this;
+
+ while (node.key !== null) {
+ output.unshift(node.key);
+ node = node.parent;
+ }
+
+ return output;
+ }
+}
+
+class PrefixTree {
+ private root: TreeNode;
+
+ constructor(){
+ this.root = new TreeNode(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 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;
+ }
+}
+
+export { PrefixTree, TreeNode };
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/symbol_encoder.ts Fri Sep 03 15:03:29 2021 +0200
@@ -0,0 +1,86 @@
+import { TextEncoder } from 'util';
+import { PrefixTree, TreeNode } from './prefix_tree';
+
+export interface SymbolEntry
+{
+ symbol: string,
+ name: string,
+ code: number,
+ abbrevs: string[]
+}
+
+class EncodeData {
+ prefixTree: PrefixTree;
+ minLength: number;
+ maxLength: number;
+
+ constructor(origin: Uint8Array[], replacement: Uint8Array[]){
+ this.prefixTree = new PrefixTree();
+
+ 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;
+
+ this.prefixTree.insert(Array.from(entry), Array.from(replacement[i]));
+ }
+ }
+}
+
+export class SymbolEncoder {
+ private symbols: EncodeData;
+ private sequences: EncodeData;
+
+ 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)))
+ }
+ this.symbols = new EncodeData(syms, seqs);
+ this.sequences = new EncodeData(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: 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/workspaceState.ts Fri Sep 03 15:03:29 2021 +0200
@@ -0,0 +1,45 @@
+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
--- a/src/Tools/VSCode/extension/src/library.ts Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts Fri Sep 03 15:03:29 2021 +0200
@@ -2,6 +2,7 @@
import * as os from 'os';
import { TextEditor, Uri, ViewColumn, workspace, window } from 'vscode'
+import { IsabelleFSP } from './isabelle_filesystem/isabelleFSP';
/* regular expressions */
@@ -24,7 +25,7 @@
export function is_file(uri: Uri): boolean
{
- return uri.scheme === "file"
+ return uri.scheme === "file" || uri.scheme === IsabelleFSP.scheme;
}
export function find_file_editor(uri: Uri): TextEditor | undefined
@@ -47,10 +48,15 @@
return workspace.getConfiguration("isabelle").get<T>(name)
}
+export function get_replacement_mode() {
+ return get_configuration<'none' | 'non-alpha' | '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>("textColor");
+ const conf = colors[color + (light ? "_light" : "_dark")];
+ return conf;
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/output_view.ts Fri Sep 03 15:03:29 2021 +0200
@@ -0,0 +1,100 @@
+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";
+
+class OutPutViewProvider implements WebviewViewProvider {
+
+ public static readonly viewType = 'isabelle-output';
+
+ private _view?: WebviewView;
+ private content: string = '';
+
+ constructor(
+ private readonly _extensionUri: Uri,
+ ) { }
+
+ public resolveWebviewView(
+ webviewView: WebviewView,
+ context: WebviewViewResolveContext,
+ _token: CancellationToken,
+ ) {
+ this._view = webviewView;
+
+ webviewView.webview.options = {
+ // Allow scripts in the webview
+ enableScripts: true,
+
+ localResourceRoots: [
+ this._extensionUri
+ ]
+ };
+
+ webviewView.webview.html = this._getHtml(this.content);
+ webviewView.webview.onDidReceiveMessage(async message => {
+ if (message.command === "open") {
+ webviewLinkOpen(message.link);
+ }
+ });
+ }
+
+ public updateContent(content: string){
+ if(!this._view){
+ this.content = content;
+ return;
+ }
+
+ this._view.webview.html = this._getHtml(content);
+ }
+
+ private _getHtml(content: string): string {
+ return getHtmlForWebview(content, this._view.webview, this._extensionUri.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 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 _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`;
+ }
+
+ return style;
+}
+
+export { OutPutViewProvider, getHtmlForWebview, webviewLinkOpen };
\ No newline at end of file
--- a/src/Tools/VSCode/extension/src/protocol.ts Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/extension/src/protocol.ts Fri Sep 03 15:03:29 2021 +0200
@@ -1,26 +1,29 @@
'use strict';
-import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions } from 'vscode'
+import { MarkdownString } from 'vscode'
import { NotificationType } from 'vscode-languageclient';
-import * as symbol from './symbol'
-
+import { SymbolEntry } from './isabelle_filesystem/symbol_encoder';
/* decorations */
export interface DecorationOpts {
range: number[],
- hover_message?: MarkedString | MarkedString[]
+ hover_message?: MarkdownString | MarkdownString[]
}
export interface Decoration
{
- uri: string,
- "type": string,
- content: DecorationOpts[]
+ "type": string;
+ content: DecorationOpts[];
+}
+
+export interface DocumentDecorations {
+ uri: string;
+ entries: Decoration[]
}
export const decoration_type =
- new NotificationType<Decoration, void>("PIDE/decoration")
+ new NotificationType<DocumentDecorations, void>("PIDE/decoration")
/* caret handling */
@@ -52,8 +55,9 @@
export interface State_Output
{
- id: number
- content: string
+ id: number;
+ content: string;
+ auto_update: boolean;
}
export const state_output_type =
@@ -105,7 +109,7 @@
export interface Symbols
{
- entries: [symbol.Entry]
+ entries: [SymbolEntry];
}
export const symbols_type =
@@ -114,6 +118,19 @@
export const symbols_request_type =
new NotificationType<void, void>("PIDE/symbols_request")
+export interface Entries<T> {
+ entries: T[];
+}
+
+export interface SessionTheories {
+ session_name: string;
+ theories: string[]
+}
+export const session_theories_type =
+ new NotificationType<Entries<SessionTheories>, void>("PIDE/session_theories")
+
+export const session_theories_request_type =
+ new NotificationType<void | { reset: boolean }, 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 Fri Sep 03 15:03:29 2021 +0200
@@ -0,0 +1,125 @@
+import { DecorationRangeBehavior, ExtensionContext, Range,
+ TextDocument, TextEditor, window, workspace } from "vscode";
+
+const arrows = {
+ sub: '⇩',
+ super: '⇧',
+ subBegin: '⇘',
+ subEnd: '⇙',
+ superBegin: '⇗',
+ superEnd: '⇖'
+}
+const noHideList = [' ', '\n', '\r', ...Object.values(arrows)];
+
+function shouldHide(nextChar: string): boolean{
+ return !noHideList.includes(nextChar);
+}
+
+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;
+
+ if (c === open) {
+ counter++;
+ }
+ else if (c === close) {
+ counter--;
+ }
+ }
+ return closeIndex;
+}
+
+
+
+function extractRanges(doc: TextDocument) {
+ const text = doc.getText();
+ const hideRanges: Range[] = [];
+ const superscriptRanges: Range[] = [];
+ const subscriptRanges: 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;
+ }
+ }
+
+ return { hideRanges, superscriptRanges, subscriptRanges };
+}
+
+export function registerScriptDecorations(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 subscript = window.createTextEditorDecorationType({
+ //textDecoration: 'none; vertical-align: sub; font-size: .83em'
+ textDecoration: 'none; position: relative; bottom: -0.5em; font-size: 80%'
+ });
+
+ const setEditorDecs = (editor: TextEditor, doc: TextDocument) => {
+ const { hideRanges, superscriptRanges, subscriptRanges } = extractRanges(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;
+ 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
--- a/src/Tools/VSCode/extension/src/state_panel.ts Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/extension/src/state_panel.ts Fri Sep 03 15:03:29 2021 +0200
@@ -2,8 +2,11 @@
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 } from 'vscode'
+import { Uri, ExtensionContext, window, WebviewPanel, ViewColumn, Webview } from 'vscode'
+import { text_colors } from './decorations';
+import { getHtmlForWebview, webviewLinkOpen } from './output_view';
let language_client: LanguageClient
@@ -17,14 +20,15 @@
{
private state_id: number
private webview_panel: WebviewPanel
+ private _extensionPath: 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._getHtml(state.content, state.auto_update);
}
public reveal()
@@ -32,8 +36,9 @@
this.webview_panel.reveal(panel_column())
}
- constructor()
+ constructor(extensionPath: string)
{
+ this._extensionPath = extensionPath;
this.webview_panel =
window.createWebviewPanel("isabelle-state", "State", panel_column(),
{
@@ -47,20 +52,34 @@
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;
}
})
}
+
+ private _getHtml(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>
+ </div>
+ ${content}`;
+
+ return getHtmlForWebview(contentWithButtons, webview, this._extensionPath);
+ }
}
let panel: Panel
@@ -86,7 +105,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)
})
-}
+}
\ No newline at end of file
--- a/src/Tools/VSCode/extension/src/symbol.ts Tue Sep 07 22:35:44 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-'use strict';
-
-import * as library from './library'
-import { Disposable, DocumentSelector, ExtensionContext, extensions, window } from 'vscode'
-
-
-/* ASCII characters */
-
-export type Symbol = string
-
-export function is_char(s: Symbol): boolean
-{ return s.length == 1 }
-
-export function is_ascii_letter(s: Symbol): boolean
-{ return is_char(s) && "A" <= s && s <= "Z" || "a" <= s && s <= "z" }
-
-export function is_ascii_digit(s: Symbol): boolean
-{ return is_char(s) && "0" <= s && s <= "9" }
-
-export function is_ascii_quasi(s: Symbol): boolean
-{ return s == "_" || s == "'" }
-
-export function is_ascii_letdig(s: Symbol): boolean
-{ return is_ascii_letter(s) || is_ascii_digit(s) || is_ascii_quasi(s) }
-
-export function is_ascii_identifier(s: Symbol): boolean
-{
- const n = s.length
-
- let all_letdig = true
- for (const c of s) { all_letdig = all_letdig && is_ascii_letdig(c) }
-
- return n > 0 && is_ascii_letter(s.charAt(0)) && all_letdig
-}
-
-
-/* named symbols */
-
-export interface Entry
-{
- symbol: Symbol,
- name: string,
- code: number
-}
-
-let symbol_entries: [Entry]
-const names = new Map<Symbol, string>()
-const codes = new Map<Symbol, number>()
-
-export function get_name(sym: Symbol): string | undefined
-{
- return names.get(sym)
-}
-
-export function get_code(sym: Symbol): number | undefined
-{
- return codes.get(sym)
-}
-
-export function get_unicode(sym: Symbol): string
-{
- const code = get_code(sym)
- return code ? String.fromCharCode(code) : ""
-}
-
-function update_entries(entries: [Entry])
-{
- symbol_entries = entries
- names.clear
- codes.clear
- for (const entry of entries) {
- names.set(entry.symbol, entry.name)
- 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/tsconfig.json Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/extension/tsconfig.json Fri Sep 03 15:03:29 2021 +0200
@@ -9,6 +9,9 @@
"sourceMap": true,
"rootDir": "."
},
+ "include": [
+ "src/**/*"
+ ],
"exclude": [
"node_modules",
".vscode-test"
--- a/src/Tools/VSCode/src/dynamic_output.scala Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala Fri Sep 03 15:03:29 2021 +0200
@@ -35,8 +35,30 @@
else this
}
if (st1.output != output) {
- channel.write(LSP.Dynamic_Output(
- resources.output_pretty_message(Pretty.separate(st1.output))))
+ val elements3: Presentation.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
+ }
+ val htmlBody = Presentation.make_html(
+ elements3,
+ entity_link,
+ Pretty.separate(st1.output))
+
+ channel.write(LSP.Dynamic_Output(HTML.source(htmlBody).toString()))
}
st1
}
--- a/src/Tools/VSCode/src/language_server.scala Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Fri Sep 03 15:03:29 2021 +0200
@@ -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
-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),
@@ -74,7 +77,7 @@
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,
+ 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)
@@ -100,6 +103,7 @@
options: Options,
session_name: String = Language_Server.default_logic,
session_dirs: List[Path] = Nil,
+ select_dirs: List[Path] = Nil,
include_sessions: List[String] = Nil,
session_ancestor: Option[String] = None,
session_requirements: Boolean = false,
@@ -114,6 +118,20 @@
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 {
@@ -263,6 +281,8 @@
val try_session =
try {
+ load_session_theories()
+
val base_info =
Sessions.base_info(
options, session_name, dirs = session_dirs, include_sessions = include_sessions,
@@ -466,6 +486,12 @@
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()
+ }
+ channel.write(LSP.Session_Theories(session_theories))
+ }
case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
}
}
--- a/src/Tools/VSCode/src/lsp.scala Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/src/lsp.scala Fri Sep 03 15:03:29 2021 +0200
@@ -158,7 +158,10 @@
val json: JSON.T =
JSON.Object(
"textDocumentSync" -> 2,
- "completionProvider" -> JSON.Object("resolveProvider" -> false, "triggerCharacters" -> Nil),
+ "completionProvider" -> JSON.Object(
+ "resolveProvider" -> false,
+ "triggerCharacters" -> Symbol.abbrevs.map { _._2.split("") }.flatten.toSet.toList
+ ),
"hoverProvider" -> true,
"definitionProvider" -> true,
"documentHighlightProvider" -> true)
@@ -212,6 +215,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 +227,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 +289,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 +313,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 +329,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 +509,17 @@
JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
}
- sealed case class Decoration(typ: String, content: List[DecorationOpts])
+ sealed case class Decoration(decos: 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" -> decos.map(c => JSON.Object(
+ "type" -> c._1,
+ "content" -> c._2.map(_.json))
+ ))
+ )
}
@@ -549,8 +563,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 +633,35 @@
{
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))
}
}
+
+ 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
+ }
+ }
+
+ object Session_Theories {
+ def apply(session_theories: Map[String, List[String]]): JSON.T = {
+ val entries = session_theories.map { case(session_name, theories) => JSON.Object(
+ "session_name" -> session_name,
+ "theories" -> theories
+ )}
+ Notification(
+ "PIDE/session_theories",
+ JSON.Object("entries" -> entries)
+ )
+ }
+ }
}
--- a/src/Tools/VSCode/src/state_panel.scala Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Fri Sep 03 15:03:29 2021 +0200
@@ -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 */
@@ -63,15 +63,33 @@
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)
+ if(body.nonEmpty){
+ val elements3: Presentation.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
+ }
+
+ val htmlBody = Presentation.make_html(
+ elements3,
+ entity_link,
+ Pretty.separate(body))
+
+ output(HTML.source(htmlBody).toString())
+ }
})
def locate(): Unit = print_state.locate_query()
@@ -105,44 +123,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 Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Sep 03 15:03:29 2021 +0200
@@ -98,13 +98,13 @@
val syntax = model.syntax()
val syntax_completion =
- syntax.complete(history, unicode = false, explicit = true,
+ syntax.complete(history, unicode = true, 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, true, syntax_completion.map(_.range), caret_range)
if (no_completion) Nil
else {
@@ -121,8 +121,8 @@
case Some(result) =>
result.items.map(item =>
LSP.CompletionItem(
- label = item.replacement,
- detail = Some(item.description.mkString(" ")),
+ label = (Some(item.description.mkString(" ")) getOrElse(item.replacement)) + " " + item.original ,
+ text = Some(item.replacement),
range = Some(doc.range(item.range))))
}
items ::: VSCode_Spell_Checker.menu_items(rendering, caret)
@@ -234,16 +234,20 @@
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)
- yield {
- val range = model.content.doc.range(text_range)
- LSP.DecorationOpts(range,
- msgs.map(msg => LSP.MarkedString(resources.output_pretty_tooltip(msg))))
- }
- LSP.Decoration(decoration.typ, content)
+ val entries = for(deco <- decoration)
+ yield {
+ 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(entries)
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Sep 03 15:03:29 2021 +0200
@@ -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)
}