# HG changeset patch
# User wenzelm
# Date 1600627679 -7200
# Node ID 199dc903131b8744416d4b3d50a4b86b651c3784
# Parent  48254fa33d885291f240ce295318adba667523c4
clarified signature;

diff -r 48254fa33d88 -r 199dc903131b src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sun Sep 20 20:00:14 2020 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sun Sep 20 20:47:59 2020 +0200
@@ -41,8 +41,8 @@
         val (output, rc) =
           Isabelle_System.bash_output
             ("\"$ISABELLE_CSDP\" " ^
-              Bash.string (File.platform_path in_path) ^ " " ^
-              Bash.string (File.platform_path out_path));
+              File.bash_platform_path in_path ^ " " ^
+              File.bash_platform_path out_path);
         val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output)
 
         val result = if File.exists out_path then File.read out_path else ""
diff -r 48254fa33d88 -r 199dc903131b src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Sun Sep 20 20:00:14 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Sun Sep 20 20:47:59 2020 +0200
@@ -319,8 +319,8 @@
       "    ()\n" ^
       "  end;\n";
     val cmd =
-      "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^
-      " --use " ^ Bash.string (File.platform_path driver_path) ^
+      "\"$POLYML_EXE\" --use " ^ File.bash_platform_path code_path ^
+      " --use " ^ File.bash_platform_path driver_path ^
       " --eval " ^ Bash.string "main ()"
   in
     List.app (File.write code_path o snd) code_files;
@@ -478,9 +478,9 @@
     val cmd =
       "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
       Config.get ctxt ghc_options ^ " -o " ^
-      Bash.string (File.platform_path compiled_path) ^ " " ^
-      Bash.string (File.platform_path driver_path) ^ " -i" ^
-      Bash.string (File.platform_path dir)
+      File.bash_platform_path compiled_path ^ " " ^
+      File.bash_platform_path driver_path ^ " -i" ^
+      File.bash_platform_path dir
   in
     check_settings compiler ISABELLE_GHC "GHC executable";
     List.app (fn (name, code) => File.write (Path.append dir (Path.basic name)) code) code_files;
@@ -521,12 +521,10 @@
       "  }\n" ^
       "}\n"
     val compile_cmd =
-      "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ Bash.string (File.platform_path dir) ^
-      " -classpath " ^ Bash.string (File.platform_path dir) ^ " " ^
-      Bash.string (File.platform_path code_path) ^ " " ^
-      Bash.string (File.platform_path driver_path)
-    val run_cmd =
-      "isabelle_scala scala -cp " ^ Bash.string (File.platform_path dir) ^ " Test"
+      "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ File.bash_platform_path dir ^
+      " -classpath " ^ File.bash_platform_path dir ^ " " ^
+      File.bash_platform_path code_path ^ " " ^ File.bash_platform_path driver_path
+    val run_cmd = "isabelle_scala scala -cp " ^ File.bash_platform_path dir ^ " Test"
   in
     List.app (File.write code_path o snd) code_files;
     File.write driver_path driver;
diff -r 48254fa33d88 -r 199dc903131b src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML	Sun Sep 20 20:00:14 2020 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML	Sun Sep 20 20:47:59 2020 +0200
@@ -223,8 +223,7 @@
         val object_file = tmp_file (module^".o")
         val _ = File.write module_file source
         val _ =
-          Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^
-            Bash.string (File.platform_path module_file))
+          Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ File.bash_platform_path module_file)
         val _ =
           if not (File.exists object_file) then
             raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
@@ -310,8 +309,7 @@
         val _ = File.write call_file call_source
         val _ =
           Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^
-            Bash.string (File.platform_path module_file) ^ " " ^
-            Bash.string (File.platform_path call_file))
+            File.bash_platform_path module_file ^ " " ^ File.bash_platform_path call_file)
         val result = File.read result_file handle IO.Io _ =>
           raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
         val t' = parse_result arity_of result
diff -r 48254fa33d88 -r 199dc903131b src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Sep 20 20:00:14 2020 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Sep 20 20:47:59 2020 +0200
@@ -263,9 +263,9 @@
         val cmd =
           "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
             (space_implode " "
-              (map (Bash.string o File.platform_path)
+              (map File.bash_platform_path
                 (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
-          " -o " ^ Bash.string (File.platform_path executable) ^ ";"
+          " -o " ^ File.bash_platform_path executable ^ ";"
         val (_, compilation_time) =
           elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
         val _ = Quickcheck.add_timing compilation_time current_result
diff -r 48254fa33d88 -r 199dc903131b src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Sun Sep 20 20:00:14 2020 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Sun Sep 20 20:47:59 2020 +0200
@@ -50,7 +50,7 @@
 
 fun make_command command options problem_path proof_path =
   Bash.strings (command () @ options) ^ " " ^
-    Bash.string (File.platform_path problem_path) ^
+    File.bash_platform_path problem_path ^
     " > " ^ File.bash_path proof_path ^ " 2>&1"
 
 fun with_trace ctxt msg f x =
diff -r 48254fa33d88 -r 199dc903131b src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sun Sep 20 20:00:14 2020 +0200
+++ b/src/Pure/General/file.ML	Sun Sep 20 20:47:59 2020 +0200
@@ -10,6 +10,7 @@
   val platform_path: Path.T -> string
   val bash_path: Path.T -> string
   val bash_paths: Path.T list -> string
+  val bash_platform_path: Path.T -> string
   val full_path: Path.T -> Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val exists: Path.T -> bool
@@ -50,6 +51,8 @@
 val bash_path = Bash_Syntax.string o standard_path;
 val bash_paths = Bash_Syntax.strings o map standard_path;
 
+val bash_platform_path = Bash_Syntax.string o platform_path;
+
 
 (* full_path *)
 
diff -r 48254fa33d88 -r 199dc903131b src/Pure/Tools/ghc.ML
--- a/src/Pure/Tools/ghc.ML	Sun Sep 20 20:00:14 2020 +0200
+++ b/src/Pure/Tools/ghc.ML	Sun Sep 20 20:47:59 2020 +0200
@@ -85,7 +85,7 @@
     val _ = File.write template_path (project_template {depends = depends, modules = modules});
     val {rc, err, ...} =
       Bash.process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^
-        " --bare " ^ Bash.string (File.platform_path template_path));
+        " --bare " ^ File.bash_platform_path template_path);
   in if rc = 0 then () else error err end;
 
 end;