1(* Title: Pure/ML/ml_syntax.ML 2 Author: Makarius 3 4Concrete ML syntax for basic values. 5*) 6 7signature ML_SYNTAX = 8sig 9 val reserved_names: string list 10 val reserved: Name.context 11 val is_reserved: string -> bool 12 val is_identifier: string -> bool 13 val atomic: string -> string 14 val print_int: int -> string 15 val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string 16 val print_list: ('a -> string) -> 'a list -> string 17 val print_option: ('a -> string) -> 'a option -> string 18 val print_char: string -> string 19 val print_string: string -> string 20 val print_strings: string list -> string 21 val print_properties: Properties.T -> string 22 val print_position: Position.T -> string 23 val print_range: Position.range -> string 24 val make_binding: string * Position.T -> string 25 val print_indexname: indexname -> string 26 val print_class: class -> string 27 val print_sort: sort -> string 28 val print_typ: typ -> string 29 val print_term: term -> string 30 val pretty_string: int -> string -> Pretty.T 31end; 32 33structure ML_Syntax: ML_SYNTAX = 34struct 35 36(* reserved words *) 37 38val reserved_names = filter Symbol.is_ascii_identifier ML_Lex.keywords; 39val reserved = Name.make_context reserved_names; 40val is_reserved = Name.is_declared reserved; 41 42 43(* identifiers *) 44 45fun is_identifier name = 46 not (is_reserved name) andalso Symbol.is_ascii_identifier name; 47 48 49(* literal output -- unformatted *) 50 51val atomic = enclose "(" ")"; 52 53val print_int = string_of_int; 54 55fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")"; 56 57fun print_list f = enclose "[" "]" o commas o map f; 58 59fun print_option f NONE = "NONE" 60 | print_option f (SOME x) = "SOME (" ^ f x ^ ")"; 61 62fun print_chr s = 63 if Symbol.is_char s then 64 (case ord s of 65 34 => "\\\"" 66 | 92 => "\\\\" 67 | 7 => "\\a" 68 | 8 => "\\b" 69 | 9 => "\\t" 70 | 10 => "\\n" 71 | 11 => "\\v" 72 | 12 => "\\f" 73 | 13 => "\\r" 74 | c => 75 if c < 32 then "\\^" ^ chr (c + 64) 76 else if c < 127 then s 77 else "\\" ^ string_of_int c) 78 else error ("Bad character: " ^ quote s); 79 80fun print_char s = 81 if Symbol.is_char s then print_chr s 82 else if Symbol.is_utf8 s then translate_string print_chr s 83 else s; 84 85val print_string = quote o implode o map print_char o Symbol.explode; 86val print_strings = print_list print_string; 87 88val print_properties = print_list (print_pair print_string print_string); 89 90fun print_position pos = 91 "Position.of_properties " ^ print_properties (Position.properties_of pos); 92 93fun print_range range = 94 "Position.range_of_properties " ^ print_properties (Position.properties_of_range range); 95 96fun make_binding (name, pos) = 97 "Binding.make " ^ print_pair print_string print_position (name, pos); 98 99val print_indexname = print_pair print_string print_int; 100 101val print_class = print_string; 102val print_sort = print_list print_class; 103 104fun print_typ (Type arg) = "Term.Type " ^ print_pair print_string (print_list print_typ) arg 105 | print_typ (TFree arg) = "Term.TFree " ^ print_pair print_string print_sort arg 106 | print_typ (TVar arg) = "Term.TVar " ^ print_pair print_indexname print_sort arg; 107 108fun print_term (Const arg) = "Term.Const " ^ print_pair print_string print_typ arg 109 | print_term (Free arg) = "Term.Free " ^ print_pair print_string print_typ arg 110 | print_term (Var arg) = "Term.Var " ^ print_pair print_indexname print_typ arg 111 | print_term (Bound i) = "Term.Bound " ^ print_int i 112 | print_term (Abs (s, T, t)) = 113 "Term.Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")" 114 | print_term (t1 $ t2) = "Term.$ " ^ print_pair print_term print_term (t1, t2); 115 116 117(* toplevel pretty printing *) 118 119fun pretty_string max_len str = 120 let 121 val body = 122 maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str) 123 handle Fail _ => Symbol.explode str; 124 val body' = 125 if length body <= max_len then body 126 else take (Int.max (max_len, 0)) body @ ["..."]; 127 in Pretty.str (quote (implode (map print_char body'))) end; 128 129val _ = 130 ML_system_pp (fn depth => fn _ => fn str => 131 Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str)); 132 133end; 134