# HG changeset patch
# User wenzelm
# Date 1646256829 -3600
# Node ID fbff7bfd58028e3a438768fe0fcf03d920cb0569
# Parent  fa9ca4563d72e29367e134aae481201669ce2c71
clarified modules;

diff -r fa9ca4563d72 -r fbff7bfd5802 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 02 21:53:17 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 02 22:33:49 2022 +0100
@@ -2,6 +2,7 @@
 
 import * as platform from './platform'
 import * as library from './library'
+import * as file from './file'
 import * as vscode_lib from './vscode_lib'
 import * as decorations from './decorations'
 import * as preview_panel from './preview_panel'
@@ -31,11 +32,11 @@
     const isabelle_args =
       ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
         .concat(vscode_lib.get_configuration<Array<string>>("args"))
-        .concat(roots.length > 0 && workspace_dir ? ["-D", library.standard_path(workspace_dir)] : [])
+        .concat(roots.length > 0 && workspace_dir ? ["-D", file.standard_path(workspace_dir)] : [])
 
     const server_options: ServerOptions =
       platform.is_windows() ?
-        { command: library.cygwin_bash(),
+        { command: file.cygwin_bash(),
           args: ["-l", isabelle_tool, "vscode_server"].concat(isabelle_args) } :
         { command: isabelle_tool,
           args: ["vscode_server"].concat(isabelle_args) }
diff -r fa9ca4563d72 -r fbff7bfd5802 src/Tools/VSCode/extension/src/file.ts
--- a/src/Tools/VSCode/extension/src/file.ts	Wed Mar 02 21:53:17 2022 +0100
+++ b/src/Tools/VSCode/extension/src/file.ts	Wed Mar 02 22:33:49 2022 +0100
@@ -5,10 +5,132 @@
 
 'use strict';
 
+import * as path from 'path'
 import * as fs from 'fs/promises'
 import { Buffer } from 'buffer'
+import * as platform from './platform'
+import * as library from './library'
 
 
+/* Windows/Cygwin */
+
+export function cygwin_root(): string
+{
+  if (platform.is_windows) {
+    return library.getenv_strict("CYGWIN_ROOT")
+  }
+  else { return "" }
+}
+
+export function cygwin_bash(): string
+{
+  return cygwin_root() + "\\bin\\bash"
+}
+
+
+/* standard path (Cygwin or Posix) */
+
+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(library.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()
+}
+
+
+/* read */
+
 export async function read_bytes(path: string): Promise<Buffer>
 {
     return fs.readFile(path)
diff -r fa9ca4563d72 -r fbff7bfd5802 src/Tools/VSCode/extension/src/library.ts
--- a/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 21:53:17 2022 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 22:33:49 2022 +0100
@@ -6,7 +6,6 @@
 'use strict';
 
 import * as platform from './platform'
-import * as path from 'path'
 
 
 /* regular expressions */
@@ -49,119 +48,3 @@
   if (s) return s
   else throw new Error("Undefined Isabelle environment variable: " + quote(name))
 }
-
-
-/* Windows/Cygwin */
-
-export function cygwin_root(): string
-{
-  if (platform.is_windows) {
-    return getenv_strict("CYGWIN_ROOT")
-  }
-  else { return "" }
-}
-
-export function cygwin_bash(): string
-{
-  return cygwin_root() + "\\bin\\bash"
-}
-
-
-/* system path representations */
-
-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()
-}