author | wenzelm |
Mon, 10 Jan 2011 15:45:46 +0100 | |
changeset 41491 | a2ad5b824051 |
parent 41415 | 23533273220a |
child 42047 | a7a4e04b5386 |
permissions | -rw-r--r-- |
24582 | 1 |
(* Title: Pure/ML/ml_syntax.ML |
24574 | 2 |
Author: Makarius |
3 |
||
4 |
Basic ML syntax operations. |
|
5 |
*) |
|
6 |
||
7 |
signature ML_SYNTAX = |
|
8 |
sig |
|
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 |
|
30230 | 21 |
val print_properties: Properties.T -> string |
22 |
val print_position: Position.T -> string |
|
30523 | 23 |
val make_binding: string * Position.T -> string |
24574 | 24 |
val print_indexname: indexname -> string |
25 |
val print_class: class -> string |
|
26 |
val print_sort: sort -> string |
|
27 |
val print_typ: typ -> string |
|
28 |
val print_term: term -> string |
|
41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
29 |
val pretty_string: int -> string -> Pretty.T |
24574 | 30 |
end; |
31 |
||
32 |
structure ML_Syntax: ML_SYNTAX = |
|
33 |
struct |
|
34 |
||
35 |
(* reserved words *) |
|
36 |
||
24582 | 37 |
val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords; |
24574 | 38 |
val reserved = Name.make_context reserved_names; |
39 |
val is_reserved = Name.is_declared reserved; |
|
40 |
||
41 |
||
42 |
(* identifiers *) |
|
43 |
||
44 |
fun is_identifier name = |
|
45 |
not (is_reserved name) andalso Syntax.is_ascii_identifier name; |
|
46 |
||
47 |
||
48 |
(* literal output -- unformatted *) |
|
49 |
||
50 |
val atomic = enclose "(" ")"; |
|
51 |
||
41491 | 52 |
val print_int = string_of_int; |
24574 | 53 |
|
54 |
fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")"; |
|
55 |
||
56 |
fun print_list f = enclose "[" "]" o commas o map f; |
|
57 |
||
58 |
fun print_option f NONE = "NONE" |
|
59 |
| print_option f (SOME x) = "SOME (" ^ f x ^ ")"; |
|
60 |
||
61 |
fun print_char s = |
|
31543
5bef6c7cc819
allow Isabelle symbols within low-level ML source;
wenzelm
parents:
30523
diff
changeset
|
62 |
if not (Symbol.is_char s) then s |
24574 | 63 |
else if s = "\"" then "\\\"" |
64 |
else if s = "\\" then "\\\\" |
|
39514
d9cf3f833318
ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
wenzelm
parents:
37535
diff
changeset
|
65 |
else if s = "\t" then "\\t" |
d9cf3f833318
ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
wenzelm
parents:
37535
diff
changeset
|
66 |
else if s = "\n" then "\\n" |
d9cf3f833318
ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
wenzelm
parents:
37535
diff
changeset
|
67 |
else if s = "\r" then "\\r" |
24574 | 68 |
else |
69 |
let val c = ord s in |
|
70 |
if c < 32 then "\\^" ^ chr (c + ord "@") |
|
71 |
else if c < 127 then s |
|
72 |
else "\\" ^ string_of_int c |
|
73 |
end; |
|
74 |
||
31543
5bef6c7cc819
allow Isabelle symbols within low-level ML source;
wenzelm
parents:
30523
diff
changeset
|
75 |
val print_string = quote o implode o map print_char o Symbol.explode; |
24574 | 76 |
val print_strings = print_list print_string; |
77 |
||
30230 | 78 |
val print_properties = print_list (print_pair print_string print_string); |
79 |
fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos); |
|
30523 | 80 |
fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos); |
30230 | 81 |
|
24574 | 82 |
val print_indexname = print_pair print_string print_int; |
83 |
||
84 |
val print_class = print_string; |
|
85 |
val print_sort = print_list print_class; |
|
86 |
||
87 |
fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg |
|
88 |
| print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg |
|
89 |
| print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg; |
|
90 |
||
91 |
fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg |
|
92 |
| print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg |
|
93 |
| print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg |
|
94 |
| print_term (Bound i) = "Bound " ^ print_int i |
|
95 |
| print_term (Abs (s, T, t)) = |
|
96 |
"Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")" |
|
97 |
| print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2); |
|
98 |
||
37535
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
99 |
|
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
100 |
(* toplevel pretty printing *) |
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
101 |
|
41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
102 |
fun pretty_string max_len str = |
37535
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
103 |
let |
41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
104 |
val body = |
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
105 |
maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str) |
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
106 |
handle Fail _ => Symbol.explode str; |
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
107 |
val body' = |
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
108 |
if length body <= max_len then body |
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
109 |
else take max_len body @ ["..."]; |
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
110 |
in Pretty.str (quote (implode (map print_char body'))) end; |
37535
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
111 |
|
24574 | 112 |
end; |