# HG changeset patch
# User haftmann
# Date 1422430148 -3600
# Node ID 180555df34ea53c21a602e5ca8017da939bc5135
# Parent  2bd467b71d15e39b6f458a92fc0e0fe4484369b6
string printing conformant to both (S)ML and Isabelle/ML

diff -r 2bd467b71d15 -r 180555df34ea src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Wed Jan 28 14:24:29 2015 +0100
+++ b/src/Tools/Code/code_ml.ML	Wed Jan 28 08:29:08 2015 +0100
@@ -51,6 +51,11 @@
 
 (** SML serializer **)
 
+fun print_char_any_ml s =
+  if Symbol.is_char s then ML_Syntax.print_char s else "\\092" ^ unprefix "\\" s;
+
+val print_string_any_ml = quote o implode o map print_char_any_ml o Symbol.explode;
+
 fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
     val deresolve_const = deresolve o Constant;
@@ -250,7 +255,7 @@
             @ "="
             :: "raise"
             :: "Fail"
-            @@ ML_Syntax.print_string const
+            @@ print_string_any_ml const
           ))
       | print_stmt _ (ML_Val binding) =
           let
@@ -354,7 +359,7 @@
 
 val literals_sml = Literals {
   literal_char = prefix "#" o quote o ML_Syntax.print_char,
-  literal_string = quote o translate_string ML_Syntax.print_char,
+  literal_string = print_string_any_ml,
   literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   literal_list = enum "," "[" "]",
   infix_cons = (7, "::")