support system path representations (as in Isabelle/Java/Scala);

--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 02 12:29:57 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 02 15:04:59 2022 +0100
@@ -35,7 +35,7 @@
 
     const server_options: ServerOptions =
       platform.is_windows() ?
-        { command: library.getenv_strict("CYGWIN_ROOT") + "\\bin\\bash",
+        { 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	Wed Mar 02 12:29:57 2022 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 15:04:59 2022 +0100
@@ -1,5 +1,7 @@
 'use strict';
 
+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'
 
@@ -45,6 +47,114 @@
 }
 
 
+/* 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("") }
+
+  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()
+}
+
+
 /* files */
 
 export function is_file(uri: Uri): boolean