# HG changeset patch
# User wenzelm
# Date 1439906927 -7200
# Node ID e08d868ceca9a12a7a71d6ede3bb4939118eb38f
# Parent  8fa408a560a5ac2746cf31d35dfa3662990d6e84
clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations);
avoid patching of SML basis library;

diff -r 8fa408a560a5 -r e08d868ceca9 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Tue Aug 18 15:37:50 2015 +0200
+++ b/src/Pure/General/file.ML	Tue Aug 18 16:08:47 2015 +0200
@@ -6,6 +6,7 @@
 
 signature FILE =
 sig
+  val standard_path: Path.T -> string
   val platform_path: Path.T -> string
   val shell_quote: string -> string
   val shell_path: Path.T -> string
@@ -42,15 +43,16 @@
 
 (* system path representations *)
 
-val platform_path = Path.implode o Path.expand;
+val standard_path = Path.implode o Path.expand;
+val platform_path = ml_platform_path o standard_path;
 
 val shell_quote = enclose "'" "'";
-val shell_path = shell_quote o platform_path;
+val shell_path = shell_quote o standard_path;
 
 
 (* current working directory *)
 
-val cd = cd o platform_path;
+val cd = cd o standard_path;
 val pwd = Path.explode o pwd;
 
 
diff -r 8fa408a560a5 -r e08d868ceca9 src/Pure/General/sha1_polyml.ML
--- a/src/Pure/General/sha1_polyml.ML	Tue Aug 18 15:37:50 2015 +0200
+++ b/src/Pure/General/sha1_polyml.ML	Tue Aug 18 16:08:47 2015 +0200
@@ -32,7 +32,7 @@
     val digest = CInterface.alloc 20 CInterface.Cchar;
     val _ =
       CInterface.call3
-        (CInterface.get_sym (ml_platform_path (File.platform_path lib_path)) "sha1_buffer")
+        (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
         (STRING_INPUT_BYTES, CInterface.LONG, CInterface.POINTER)
         CInterface.POINTER (str, size str, CInterface.address digest);
   in fold (suffix o hex_string digest) (0 upto 19) "" end;
diff -r 8fa408a560a5 -r e08d868ceca9 src/Pure/ML-Systems/windows_polyml.ML
--- a/src/Pure/ML-Systems/windows_polyml.ML	Tue Aug 18 15:37:50 2015 +0200
+++ b/src/Pure/ML-Systems/windows_polyml.ML	Tue Aug 18 16:08:47 2015 +0200
@@ -33,44 +33,3 @@
       | _ => path')
     else path'
   end;
-
-structure OS =
-struct
-  open OS;
-
-  structure FileSys =
-  struct
-    open FileSys;
-
-    val openDir = openDir o ml_platform_path;
-
-    val chDir = chDir o ml_platform_path;
-    val getDir = ml_standard_path o getDir;
-    val mkDir = mkDir o ml_platform_path;
-    val rmDir = rmDir o ml_platform_path;
-    val isDir = isDir o ml_platform_path;
-    val isLink = isLink o ml_platform_path;
-    val readLink = readLink o ml_platform_path;
-    val fullPath = ml_standard_path o fullPath o ml_platform_path;
-    val realPath = ml_standard_path o realPath o ml_platform_path;
-    val modTime = modTime o ml_platform_path;
-    val fileSize = fileSize o ml_platform_path;
-    fun setTime (file, time) = FileSys.setTime (ml_platform_path file, time);
-    val remove = remove o ml_platform_path;
-    fun rename {old, new} = FileSys.rename {old = ml_platform_path old, new = ml_platform_path new};
-
-    fun access (file, modes) = FileSys.access (ml_platform_path file, modes);
-
-    val tmpName = ml_standard_path o tmpName;
-
-    val fileId = fileId o ml_platform_path;
-  end;
-end;
-
-structure TextIO =
-struct
-  open TextIO;
-  val openIn = openIn o ml_platform_path;
-  val openOut = openOut o ml_platform_path;
-  val openAppend = openAppend o ml_platform_path;
-end;
diff -r 8fa408a560a5 -r e08d868ceca9 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Tue Aug 18 15:37:50 2015 +0200
+++ b/src/Pure/System/isabelle_system.ML	Tue Aug 18 16:08:47 2015 +0200
@@ -41,14 +41,17 @@
 
 fun isabelle_tool name args =
   (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
-      let val path = File.platform_path (Path.append (Path.explode dir) (Path.basic name)) in
-        if can OS.FileSys.modTime path andalso
-          not (OS.FileSys.isDir path) andalso
-          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
+      let
+        val path = Path.append (Path.explode dir) (Path.basic name);
+        val platform_path = File.platform_path path;
+      in
+        if can OS.FileSys.modTime platform_path andalso
+          not (OS.FileSys.isDir platform_path) andalso
+          OS.FileSys.access (platform_path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
         then SOME path
         else NONE
       end handle OS.SysErr _ => NONE) of
-    SOME path => bash (File.shell_quote path ^ " " ^ args)
+    SOME path => bash (File.shell_path path ^ " " ^ args)
   | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
 
 fun system_command cmd =
diff -r 8fa408a560a5 -r e08d868ceca9 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Aug 18 15:37:50 2015 +0200
+++ b/src/Pure/library.ML	Tue Aug 18 16:08:47 2015 +0200
@@ -1029,8 +1029,8 @@
 
 (* current directory *)
 
-val cd = OS.FileSys.chDir;
-val pwd = OS.FileSys.getDir;
+val cd = OS.FileSys.chDir o ml_platform_path;
+val pwd = ml_standard_path o OS.FileSys.getDir;
 
 
 (* getenv *)