# 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;