# HG changeset patch
# User wenzelm
# Date 1600972147 -7200
# Node ID ccc104786829c0a93f687d9fd5aac11872b3ba14
# Parent  811d5eec65a6b4e5960452a79f3fbba9c024c9c6
tuned;

diff -r 811d5eec65a6 -r ccc104786829 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu Sep 24 19:54:12 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Sep 24 20:29:07 2020 +0200
@@ -347,15 +347,15 @@
     val code_path = Path.append dir (Path.basic generatedN)
     val driver_path = Path.append dir (Path.basic driverN)
     val basis_path = Path.append dir (Path.basic (projectN ^ ".mlb"))
-    val driver =
-      "fun format_term NONE = \"\"\n" ^
-      "  | format_term (SOME t) = t ();\n" ^
-      "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
-      "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
-      "val result = " ^ value_name ^ " ();\n" ^
-      "val _ = print \"" ^ start_markerN ^ "\";\n" ^
-      "val _ = map (print o format) result;\n" ^
-      "val _ = print \"" ^ end_markerN ^ "\";\n"
+    val driver = \<^verbatim>\<open>
+fun format (true, _) = \<close> ^ ML_Syntax.print_string successN ^ \<^verbatim>\<open> ^ "\n"
+  | format (false, NONE) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ "\n"
+  | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ t () ^ "\n"
+val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
+val _ = print \<close> ^ ML_Syntax.print_string start_markerN ^ \<^verbatim>\<open>
+val _ = List.app (print o format) result
+val _ = print \<close> ^ ML_Syntax.print_string end_markerN ^ \<^verbatim>\<open>
+\<close>
     val cmd = "\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path
   in
     check_settings compiler ISABELLE_MLTON "MLton executable";
@@ -380,22 +380,21 @@
 
     val code_path = Path.append dir (Path.basic generatedN)
     val driver_path = Path.append dir (Path.basic driverN)
-    val driver =
-      "structure Test = struct\n" ^
-      "fun main () =\n" ^
-      "  let\n" ^
-      "    fun format_term NONE = \"\"\n" ^
-      "      | format_term (SOME t) = t ();\n" ^
-      "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
-      "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
-      "    val result = " ^ value_name ^ " ();\n" ^
-      "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
-      "    val _ = map (print o format) result;\n" ^
-      "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
-      "  in\n" ^
-      "    0\n" ^
-      "  end;\n" ^
-      "end;"
+    val driver = \<^verbatim>\<open>
+structure Test =
+struct
+  fun main () =
+    let
+      fun format (true, _) = \<close> ^ ML_Syntax.print_string successN ^ \<^verbatim>\<open> ^ "\n"
+        | format (false, NONE) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ "\n"
+        | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ t () ^ "\n"
+      val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
+      val _ = print \<close> ^ ML_Syntax.print_string start_markerN ^ \<^verbatim>\<open>
+      val _ = List.app (print o format) result
+      val _ = print \<close> ^ ML_Syntax.print_string end_markerN ^ \<^verbatim>\<open>
+    in 0 end
+end
+\<close>
     val ml_source =
       "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
       "use " ^ ML_Syntax.print_string (File.platform_path code_path) ^