--- a/lib/Tools/vscode Tue Mar 01 15:05:27 2022 +0000
+++ b/lib/Tools/vscode Wed Mar 02 15:08:49 2022 +0100
@@ -6,6 +6,7 @@
DIR="$(isabelle vscode_setup -C)" || exit "$?"
exec "$DIR/bin/codium" \
+ --locale en-US \
--user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \
--extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \
"$@"
--- a/src/Tools/VSCode/extension/package-lock.json Tue Mar 01 15:05:27 2022 +0000
+++ b/src/Tools/VSCode/extension/package-lock.json Wed Mar 02 15:08:49 2022 +0100
@@ -874,9 +874,9 @@
}
},
"node_modules/typescript": {
- "version": "4.5.5",
- "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.5.5.tgz",
- "integrity": "sha512-TCTIul70LyWe6IJWT8QSYeA54WQe8EjQFU4wY52Fasj5UKx88LNYKCgBEHcOMOrFF1rKGbD8v/xcNWVUq9SymA==",
+ "version": "4.6.2",
+ "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.6.2.tgz",
+ "integrity": "sha512-HM/hFigTBHZhLXshn9sN37H085+hQGeJHJ/X7LpBWLID/fbc2acUMfU+lGD98X81sKP+pFa9f0DZmCwB9GnbAg==",
"dev": true,
"bin": {
"tsc": "bin/tsc",
@@ -1638,9 +1638,9 @@
}
},
"typescript": {
- "version": "4.5.5",
- "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.5.5.tgz",
- "integrity": "sha512-TCTIul70LyWe6IJWT8QSYeA54WQe8EjQFU4wY52Fasj5UKx88LNYKCgBEHcOMOrFF1rKGbD8v/xcNWVUq9SymA==",
+ "version": "4.6.2",
+ "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.6.2.tgz",
+ "integrity": "sha512-HM/hFigTBHZhLXshn9sN37H085+hQGeJHJ/X7LpBWLID/fbc2acUMfU+lGD98X81sKP+pFa9f0DZmCwB9GnbAg==",
"dev": true
},
"vscode-jsonrpc": {
--- a/src/Tools/VSCode/extension/package.json Tue Mar 01 15:05:27 2022 +0000
+++ b/src/Tools/VSCode/extension/package.json Wed Mar 02 15:08:49 2022 +0100
@@ -23,14 +23,7 @@
"Programming Languages"
],
"activationEvents": [
- "workspaceContains:ROOT",
- "workspaceContains:ROOTS",
- "onLanguage:isabelle",
- "onLanguage:isabelle-ml",
- "onLanguage:bibtex",
- "onCommand:isabelle.state",
- "onCommand:isabelle.preview",
- "onCommand:isabelle.preview-split"
+ "onStartupFinished"
],
"main": "./out/src/extension",
"contributes": {
--- a/src/Tools/VSCode/extension/src/extension.ts Tue Mar 01 15:05:27 2022 +0000
+++ b/src/Tools/VSCode/extension/src/extension.ts Wed Mar 02 15:08:49 2022 +0100
@@ -1,6 +1,6 @@
'use strict';
-import * as path from 'path'
+import * as platform from './platform'
import * as library from './library'
import * as decorations from './decorations'
import * as preview_panel from './preview_panel'
@@ -34,8 +34,8 @@
.concat(roots.length > 0 && workspace_dir !== undefined ? ["-D", workspace_dir] : [])
const server_options: ServerOptions =
- library.platform_is_windows() ?
- { command: library.getenv_strict("CYGWIN_ROOT") + "\\bin\\bash",
+ platform.is_windows() ?
+ { command: library.cygwin_root() + "\\bin\\bash",
args: ["-l", isabelle_tool, "vscode_server"].concat(isabelle_args) } :
{ command: isabelle_tool,
args: ["vscode_server"].concat(isabelle_args) }
--- a/src/Tools/VSCode/extension/src/library.ts Tue Mar 01 15:05:27 2022 +0000
+++ b/src/Tools/VSCode/extension/src/library.ts Wed Mar 02 15:08:49 2022 +0100
@@ -1,6 +1,7 @@
'use strict';
-import * as os from 'os'
+import * as platform from './platform'
+import * as path from 'path'
import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode'
import {Isabelle_Workspace} from './isabelle_filesystem/isabelle_workspace'
@@ -9,9 +10,10 @@
export function escape_regex(s: string): string
{
- return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&")
+ return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&").replace(/-/g, "\\x2d")
}
+
/* strings */
export function quote(s: string): string
@@ -46,11 +48,111 @@
}
-/* platform information */
+/* system path representations */
+
+export function cygwin_root(): string
+{
+ if (platform.is_windows) {
+ return getenv_strict("CYGWIN_ROOT")
+ }
+ else { return "" }
+}
+
+function slashes(s: string): string
+{
+ return s.replace(/\\/g, "/")
+}
+
+export function standard_path(platform_path: string): string
+{
+ if (platform.is_windows()) {
+ const backslashes = platform_path.replace(/\//g, "\\")
+
+ const root_pattern = new RegExp(escape_regex(cygwin_root()) + "(?:\\\\+|\\z)(.*)", "i")
+ const root_match = backslashes.match(root_pattern)
+
+ const drive_pattern = new RegExp("([a-zA-Z]):\\\\*(.*)")
+ const drive_match = backslashes.match(drive_pattern)
+
+ if (root_match) {
+ const rest = root_match[1]
+ return "/" + slashes(rest)
+ }
+ else if (drive_match) {
+ const letter = drive_match[1].toLowerCase()
+ const rest = drive_match[2]
+ return "/cygdrive/" + letter + (!rest ? "" : "/" + slashes(rest))
+ }
+ else { return slashes(backslashes) }
+ }
+ else { return platform_path }
+}
+
+export function platform_path(standard_path: string): string
+{
+ var _result = []
+ function result(): string { return _result.join("") }
-export function platform_is_windows(): boolean
-{
- return os.type().startsWith("Windows")
+ function clear(): void { _result = [] }
+ function add(s: string): void { _result.push(s) }
+ function separator(): void
+ {
+ const n = _result.length
+ if (n > 0 && _result[n - 1] !== path.sep) {
+ add(path.sep)
+ }
+ }
+
+
+ // check root
+
+ var rest = standard_path
+ const is_root = standard_path.startsWith("/")
+
+ if (platform.is_windows) {
+ const cygdrive_pattern = new RegExp("/cygdrive/([a-zA-Z])($|/.*)")
+ const cygdrive_match = standard_path.match(cygdrive_pattern)
+
+ const named_root_pattern = new RegExp("//+([^/]*)(.*)")
+ const named_root_match = standard_path.match(named_root_pattern)
+
+ if (cygdrive_match) {
+ const drive = cygdrive_match[1].toUpperCase()
+ rest = cygdrive_match[2]
+ clear()
+ add(drive)
+ add(":")
+ add(path.sep)
+ }
+ else if (named_root_match) {
+ const root = named_root_match[1]
+ rest = named_root_match[2]
+ clear()
+ add(path.sep)
+ add(path.sep)
+ add(root)
+ }
+ else if (is_root) {
+ clear()
+ add(cygwin_root())
+ }
+ }
+ else if (is_root) {
+ clear()
+ add(path.sep)
+ }
+
+
+ // check rest
+
+ for (const p of rest.split("/")) {
+ if (p) {
+ separator()
+ add(p)
+ }
+ }
+
+ return result()
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/platform.ts Wed Mar 02 15:08:49 2022 +0100
@@ -0,0 +1,26 @@
+'use strict';
+
+import * as os from 'os'
+
+
+/* platform family */
+
+export function is_windows(): boolean
+{
+ return os.type().startsWith("Windows")
+}
+
+export function is_linux(): boolean
+{
+ return os.type().startsWith("Linux")
+}
+
+export function is_macos(): boolean
+{
+ return os.type().startsWith("Darwin")
+}
+
+export function is_unix(): boolean
+{
+ return is_linux() || is_macos()
+}
--- a/src/Tools/VSCode/src/vscode_setup.scala Tue Mar 01 15:05:27 2022 +0000
+++ b/src/Tools/VSCode/src/vscode_setup.scala Wed Mar 02 15:08:49 2022 +0100
@@ -81,6 +81,7 @@
"editor.lineNumbers": "off",
"editor.renderIndentGuides": false,
"editor.rulers": [80, 100],
+ "editor.unicodeHighlight.ambiguousCharacters": false,
"extensions.autoCheckUpdates": false,
"extensions.autoUpdate": false,
"update.mode": "none"