--- 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) }
--- 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)
--- 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()
-}