# HG changeset patch
# User wenzelm
# Date 1600967087 -7200
# Node ID 03628da91b0720cdd2f3cd2d7107a7f1ec48a921
# Parent  697e5688f37073b9790dd87bbbb4821ef9d0be17
proper platform_path for Windows;

diff -r 697e5688f370 -r 03628da91b07 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu Sep 24 17:23:25 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Sep 24 19:04:47 2020 +0200
@@ -311,7 +311,7 @@
       string start_markerN ^
       \<^verbatim>\<open> ^ String.concat (map format result) ^ \<close> ^
       string end_markerN ^ \<^verbatim>\<open>
-    val out = BinIO.openOut \<close> ^ string (Path.implode (Path.expand out_path)) ^ \<^verbatim>\<open>
+    val out = BinIO.openOut \<close> ^ ML_Syntax.print_platform_path out_path ^ \<^verbatim>\<open>
     val _ = BinIO.output (out, Byte.stringToBytes result_text)
     val _ = BinIO.closeOut out
   in () end;
diff -r 697e5688f370 -r 03628da91b07 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Thu Sep 24 17:23:25 2020 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Thu Sep 24 19:04:47 2020 +0200
@@ -20,6 +20,7 @@
   val print_string: string -> string
   val print_strings: string list -> string
   val print_path: Path.T -> string
+  val print_platform_path: Path.T -> string
   val print_properties: Properties.T -> string
   val print_position: Position.T -> string
   val print_range: Position.range -> string
@@ -91,6 +92,8 @@
 fun print_path path =
   "Path.explode " ^ print_string (Path.implode path);
 
+val print_platform_path = print_string o File.platform_path;
+
 val print_properties = print_list (print_pair print_string print_string);
 
 fun print_position pos =