src/Pure/ML/ml_syntax.ML
changeset 62528 c8c532b22947
parent 58978 e42da880c61e
child 62663 bea354f6ff21
equal deleted inserted replaced
62527:aae9a2a855e0 62528:c8c532b22947
     1 (*  Title:      Pure/ML/ml_syntax.ML
     1 (*  Title:      Pure/ML/ml_syntax.ML
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 Basic ML syntax operations.
     4 Concrete ML syntax for basic values.
     5 *)
     5 *)
     6 
     6 
     7 signature ML_SYNTAX =
     7 signature ML_SYNTAX =
     8 sig
     8 sig
     9   val reserved_names: string list
     9   val reserved_names: string list
    57 fun print_list f = enclose "[" "]" o commas o map f;
    57 fun print_list f = enclose "[" "]" o commas o map f;
    58 
    58 
    59 fun print_option f NONE = "NONE"
    59 fun print_option f NONE = "NONE"
    60   | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
    60   | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
    61 
    61 
       
    62 fun print_chr s =
       
    63   if Symbol.is_char s then
       
    64     (case ord s of
       
    65       34 => "\\\""
       
    66     | 92 => "\\\\"
       
    67     | 9 => "\\t"
       
    68     | 10 => "\\n"
       
    69     | 11 => "\\f"
       
    70     | 13 => "\\r"
       
    71     | c =>
       
    72         if c < 32 then "\\^" ^ chr (c + 64)
       
    73         else if c < 127 then s
       
    74         else "\\" ^ string_of_int c)
       
    75   else error ("Bad character: " ^ quote s);
       
    76 
    62 fun print_char s =
    77 fun print_char s =
    63   if not (Symbol.is_char s) then s
    78   if Symbol.is_char s then print_chr s
    64   else if s = "\"" then "\\\""
    79   else if Symbol.is_utf8 s then translate_string print_chr s
    65   else if s = "\\" then "\\\\"
    80   else s;
    66   else if s = "\t" then "\\t"
       
    67   else if s = "\n" then "\\n"
       
    68   else if s = "\f" then "\\f"
       
    69   else if s = "\r" then "\\r"
       
    70   else
       
    71     let val c = ord s in
       
    72       if c < 32 then "\\^" ^ chr (c + ord "@")
       
    73       else if c < 127 then s
       
    74       else "\\" ^ string_of_int c
       
    75     end;
       
    76 
    81 
    77 val print_string = quote o implode o map print_char o Symbol.explode;
    82 val print_string = quote o implode o map print_char o Symbol.explode;
    78 val print_strings = print_list print_string;
    83 val print_strings = print_list print_string;
    79 
    84 
    80 val print_properties = print_list (print_pair print_string print_string);
    85 val print_properties = print_list (print_pair print_string print_string);