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