# HG changeset patch
# User wenzelm
# Date 1540910724 -3600
# Node ID ae2074acbaa88f5cca8f65513d38b80182b015d3
# Parent  a5c0d61ce5dbfad0324005a2de22db9e67e8560d
clarified signature;

diff -r a5c0d61ce5db -r ae2074acbaa8 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Sun Oct 28 16:31:13 2018 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Tue Oct 30 15:45:24 2018 +0100
@@ -15,7 +15,8 @@
   val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
   val print_list: ('a -> string) -> 'a list -> string
   val print_option: ('a -> string) -> 'a option -> string
-  val print_char: string -> string
+  val print_symbol_char: Symbol.symbol -> string
+  val print_symbol: Symbol.symbol -> string
   val print_string: string -> string
   val print_strings: string list -> string
   val print_properties: Properties.T -> string
@@ -59,7 +60,7 @@
 fun print_option f NONE = "NONE"
   | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
 
-fun print_chr s =
+fun print_symbol_char s =
   if Symbol.is_char s then
     (case ord s of
       34 => "\\\""
@@ -77,12 +78,12 @@
         else "\\" ^ string_of_int c)
   else error ("Bad character: " ^ quote s);
 
-fun print_char s =
-  if Symbol.is_char s then print_chr s
-  else if Symbol.is_utf8 s then translate_string print_chr s
+fun print_symbol s =
+  if Symbol.is_char s then print_symbol_char s
+  else if Symbol.is_utf8 s then translate_string print_symbol_char s
   else s;
 
-val print_string = quote o implode o map print_char o Symbol.explode;
+val print_string = quote o implode o map print_symbol o Symbol.explode;
 val print_strings = print_list print_string;
 
 val print_properties = print_list (print_pair print_string print_string);
@@ -124,7 +125,7 @@
     val body' =
       if length body <= max_len then body
       else take (Int.max (max_len, 0)) body @ ["..."];
-  in Pretty.str (quote (implode (map print_char body'))) end;
+  in Pretty.str (quote (implode (map print_symbol body'))) end;
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn str =>
diff -r a5c0d61ce5db -r ae2074acbaa8 src/Pure/Thy/markdown.ML
--- a/src/Pure/Thy/markdown.ML	Sun Oct 28 16:31:13 2018 +0100
+++ b/src/Pure/Thy/markdown.ML	Tue Oct 30 15:45:24 2018 +0100
@@ -84,7 +84,7 @@
   (case bad_blanks source of
     [] => ()
   | (c, pos) :: _ =>
-      error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
+      error ("Bad blank character " ^ quote (ML_Syntax.print_symbol c) ^ Position.here pos));
 
 val is_space = Symbol.is_space o Symbol_Pos.symbol;
 val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
diff -r a5c0d61ce5db -r ae2074acbaa8 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sun Oct 28 16:31:13 2018 +0100
+++ b/src/Tools/Code/code_haskell.ML	Tue Oct 30 15:45:24 2018 +0100
@@ -41,7 +41,7 @@
       let
         val _ = if Symbol.is_ascii c then ()
           else error "non-ASCII byte in Haskell string literal";
-        val s = ML_Syntax.print_char c;
+        val s = ML_Syntax.print_symbol_char c;
       in if s = "'" then "\\'" else s end;
   in quote o translate_string char end;
 
diff -r a5c0d61ce5db -r ae2074acbaa8 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Oct 28 16:31:13 2018 +0100
+++ b/src/Tools/Code/code_ml.ML	Tue Oct 30 15:45:24 2018 +0100
@@ -55,7 +55,7 @@
   if c = "\\"
   then "\\092" (*produce strings suitable for both SML as well as Isabelle/ML*)
   else if Symbol.is_ascii c
-  then ML_Syntax.print_char c
+  then ML_Syntax.print_symbol_char c
   else error "non-ASCII byte in SML string literal";
 
 val print_sml_string = quote o translate_string print_sml_char;