# HG changeset patch
# User wenzelm
# Date 1646230129 -3600
# Node ID 74f0110bbd0a5c2c60e964cee39ec1c543bdcc5e
# Parent  ff60b4acd6ddf22d187162fa0cc79e72e49b7f72# Parent  e3388efdacd7d9b0aabaef9820e6d8b1e39c8b6b
merged

diff -r ff60b4acd6dd -r 74f0110bbd0a lib/Tools/vscode
--- 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)" \
   "$@"
diff -r ff60b4acd6dd -r 74f0110bbd0a src/Tools/VSCode/extension/package-lock.json
--- 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": {
diff -r ff60b4acd6dd -r 74f0110bbd0a src/Tools/VSCode/extension/package.json
--- 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": {
diff -r ff60b4acd6dd -r 74f0110bbd0a src/Tools/VSCode/extension/src/extension.ts
--- 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) }
diff -r ff60b4acd6dd -r 74f0110bbd0a src/Tools/VSCode/extension/src/library.ts
--- 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()
 }
 
 
diff -r ff60b4acd6dd -r 74f0110bbd0a src/Tools/VSCode/extension/src/platform.ts
--- /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()
+}
diff -r ff60b4acd6dd -r 74f0110bbd0a src/Tools/VSCode/src/vscode_setup.scala
--- 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"