# HG changeset patch
# User wenzelm
# Date 1646334823 -3600
# Node ID d2add317268f6c22349964f5a2092907717dabcf
# Parent  4187f6f18232b075d2c9b1f75de17faf25caaf92
clarified signature: file operations take standard_path as in Isabelle/ML/Scala;

diff -r 4187f6f18232 -r d2add317268f src/Tools/VSCode/extension/src/file.ts
--- a/src/Tools/VSCode/extension/src/file.ts	Thu Mar 03 20:04:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/file.ts	Thu Mar 03 20:13:43 2022 +0100
@@ -61,6 +61,8 @@
 }
 
 
+/* platform path (Windows or Posix) */
+
 export function platform_path(standard_path: string): string
 {
   var _result = []
@@ -133,7 +135,7 @@
 
 export async function read_bytes(path: string): Promise<Buffer>
 {
-    return fs.readFile(path)
+    return fs.readFile(platform_path(path))
 }
 
 export async function read(path: string): Promise<string>
diff -r 4187f6f18232 -r d2add317268f src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Thu Mar 03 20:04:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Thu Mar 03 20:13:43 2022 +0100
@@ -83,6 +83,6 @@
 
 export async function load_symbols(path: string): Promise<Symbols>
 {
-  const entries = await file.read_json<[Entry]>(file.platform_path(path))
+  const entries = await file.read_json<[Entry]>(path)
   return new Symbols(entries)
 }