clarified signature;
authorwenzelm
Tue Oct 30 15:45:24 2018 +0100 (9 months ago)
changeset 69207ae2074acbaa8
parent 69203 a5c0d61ce5db
child 69208 3e4edf43e254
clarified signature;
src/Pure/ML/ml_syntax.ML
src/Pure/Thy/markdown.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
     1.1 --- a/src/Pure/ML/ml_syntax.ML	Sun Oct 28 16:31:13 2018 +0100
     1.2 +++ b/src/Pure/ML/ml_syntax.ML	Tue Oct 30 15:45:24 2018 +0100
     1.3 @@ -15,7 +15,8 @@
     1.4    val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
     1.5    val print_list: ('a -> string) -> 'a list -> string
     1.6    val print_option: ('a -> string) -> 'a option -> string
     1.7 -  val print_char: string -> string
     1.8 +  val print_symbol_char: Symbol.symbol -> string
     1.9 +  val print_symbol: Symbol.symbol -> string
    1.10    val print_string: string -> string
    1.11    val print_strings: string list -> string
    1.12    val print_properties: Properties.T -> string
    1.13 @@ -59,7 +60,7 @@
    1.14  fun print_option f NONE = "NONE"
    1.15    | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
    1.16  
    1.17 -fun print_chr s =
    1.18 +fun print_symbol_char s =
    1.19    if Symbol.is_char s then
    1.20      (case ord s of
    1.21        34 => "\\\""
    1.22 @@ -77,12 +78,12 @@
    1.23          else "\\" ^ string_of_int c)
    1.24    else error ("Bad character: " ^ quote s);
    1.25  
    1.26 -fun print_char s =
    1.27 -  if Symbol.is_char s then print_chr s
    1.28 -  else if Symbol.is_utf8 s then translate_string print_chr s
    1.29 +fun print_symbol s =
    1.30 +  if Symbol.is_char s then print_symbol_char s
    1.31 +  else if Symbol.is_utf8 s then translate_string print_symbol_char s
    1.32    else s;
    1.33  
    1.34 -val print_string = quote o implode o map print_char o Symbol.explode;
    1.35 +val print_string = quote o implode o map print_symbol o Symbol.explode;
    1.36  val print_strings = print_list print_string;
    1.37  
    1.38  val print_properties = print_list (print_pair print_string print_string);
    1.39 @@ -124,7 +125,7 @@
    1.40      val body' =
    1.41        if length body <= max_len then body
    1.42        else take (Int.max (max_len, 0)) body @ ["..."];
    1.43 -  in Pretty.str (quote (implode (map print_char body'))) end;
    1.44 +  in Pretty.str (quote (implode (map print_symbol body'))) end;
    1.45  
    1.46  val _ =
    1.47    ML_system_pp (fn depth => fn _ => fn str =>
     2.1 --- a/src/Pure/Thy/markdown.ML	Sun Oct 28 16:31:13 2018 +0100
     2.2 +++ b/src/Pure/Thy/markdown.ML	Tue Oct 30 15:45:24 2018 +0100
     2.3 @@ -84,7 +84,7 @@
     2.4    (case bad_blanks source of
     2.5      [] => ()
     2.6    | (c, pos) :: _ =>
     2.7 -      error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
     2.8 +      error ("Bad blank character " ^ quote (ML_Syntax.print_symbol c) ^ Position.here pos));
     2.9  
    2.10  val is_space = Symbol.is_space o Symbol_Pos.symbol;
    2.11  val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
     3.1 --- a/src/Tools/Code/code_haskell.ML	Sun Oct 28 16:31:13 2018 +0100
     3.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Oct 30 15:45:24 2018 +0100
     3.3 @@ -41,7 +41,7 @@
     3.4        let
     3.5          val _ = if Symbol.is_ascii c then ()
     3.6            else error "non-ASCII byte in Haskell string literal";
     3.7 -        val s = ML_Syntax.print_char c;
     3.8 +        val s = ML_Syntax.print_symbol_char c;
     3.9        in if s = "'" then "\\'" else s end;
    3.10    in quote o translate_string char end;
    3.11  
     4.1 --- a/src/Tools/Code/code_ml.ML	Sun Oct 28 16:31:13 2018 +0100
     4.2 +++ b/src/Tools/Code/code_ml.ML	Tue Oct 30 15:45:24 2018 +0100
     4.3 @@ -55,7 +55,7 @@
     4.4    if c = "\\"
     4.5    then "\\092" (*produce strings suitable for both SML as well as Isabelle/ML*)
     4.6    else if Symbol.is_ascii c
     4.7 -  then ML_Syntax.print_char c
     4.8 +  then ML_Syntax.print_symbol_char c
     4.9    else error "non-ASCII byte in SML string literal";
    4.10  
    4.11  val print_sml_string = quote o translate_string print_sml_char;