src/HOL/Library/code_test.ML

       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
       "  in\n" ^
       "    ()\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;
     File.write driver_path driver;
     evaluate compiler cmd

 
     val compiled_path = Path.append dir (Path.basic "test")
     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;
     File.write driver_path driver;
     compile compiler cmd;

       "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
       "    print(\"" ^ end_markerN ^ "\");\n" ^
       "  }\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;
     compile compiler compile_cmd;
     evaluate compiler run_cmd