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;