# HG changeset patch # User wenzelm # Date 1672756374 -3600 # Node ID d9913b41a7bc52772ca60d20f4f6d3b029f07eec # Parent b59118d11a4615784d2dd698e88a622681d4c2ad tuned; diff -r b59118d11a46 -r d9913b41a7bc src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Tue Jan 03 15:03:48 2023 +0100 +++ b/src/HOL/Library/code_test.ML Tue Jan 03 15:32:54 2023 +0100 @@ -503,7 +503,7 @@ case (false, Some(t)) => "False" + t(()) + "\n" }).mkString isabelle.File.write( - isabelle.Path.explode(\ ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\), + isabelle.Path.explode(\ ^ quote (File.standard_path out_path) ^ \<^verbatim>\), \ ^ quote start_marker ^ \<^verbatim>\ + result_text + \ ^ quote end_marker ^ \<^verbatim>\) }\ val _ = File.write code_path code diff -r b59118d11a46 -r d9913b41a7bc src/HOL/Matrix_LP/Cplex_tools.ML --- a/src/HOL/Matrix_LP/Cplex_tools.ML Tue Jan 03 15:03:48 2023 +0100 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML Tue Jan 03 15:32:54 2023 +0100 @@ -1136,7 +1136,7 @@ exception Execute of string; -fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s))); +fun tmp_file s = File.standard_path (File.tmp_path (Path.basic s)); fun wrap s = "\""^s^"\""; fun solve_glpk prog =