Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 03 Jan 2023 15:32:54 +0100
changeset 76882 d9913b41a7bc
parent 76881 b59118d11a46
child 76883 186e07be32c3
tuned;
src/HOL/Library/code_test.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Cplex_tools.ML file | annotate | diff | comparison | revisions 
--- 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(\<close> ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\<open>),
+    isabelle.Path.explode(\<close> ^ quote (File.standard_path out_path) ^ \<^verbatim>\<open>),
     \<close> ^ quote start_marker ^ \<^verbatim>\<open> + result_text + \<close> ^ quote end_marker ^ \<^verbatim>\<open>)
 }\<close>
     val _ = File.write code_path code
--- 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 =
isabelle