author | wenzelm |
Sat, 24 Mar 2018 20:51:42 +0100 | |
changeset 67945 | 984c3dc46cc0 |
parent 67556 | 5f86e2a9c59c |
child 69042 | 6e9df530b441 |
permissions | -rw-r--r-- |
18 | 1 |
(* Title: Pure/Syntax/lexicon.ML |
2 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
|
0 | 3 |
|
4703 | 4 |
Lexer for the inner Isabelle syntax (terms and types). |
18 | 5 |
*) |
0 | 6 |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
7 |
signature LEXICON = |
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
8 |
sig |
42476 | 9 |
structure Syntax: |
10 |
sig |
|
11 |
val const: string -> term |
|
12 |
val free: string -> term |
|
13 |
val var: indexname -> term |
|
14 |
end |
|
67426 | 15 |
val scan_id: Symbol_Pos.T list scanner |
16 |
val scan_longid: Symbol_Pos.T list scanner |
|
17 |
val scan_tid: Symbol_Pos.T list scanner |
|
18 |
val scan_hex: Symbol_Pos.T list scanner |
|
19 |
val scan_bin: Symbol_Pos.T list scanner |
|
20 |
val scan_var: Symbol_Pos.T list scanner |
|
21 |
val scan_tvar: Symbol_Pos.T list scanner |
|
50239 | 22 |
val is_tid: string -> bool |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
23 |
datatype token_kind = |
67548 | 24 |
Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str | |
67550 | 25 |
String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF |
67554 | 26 |
eqtype token |
67412 | 27 |
val kind_of_token: token -> token_kind |
27806 | 28 |
val str_of_token: token -> string |
29 |
val pos_of_token: token -> Position.T |
|
67551 | 30 |
val end_pos_of_token: token -> Position.T |
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
31 |
val is_proper: token -> bool |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
32 |
val dummy: token |
67552 | 33 |
val literal: string -> token |
34 |
val is_literal: token -> bool |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
35 |
val tokens_match_ord: token * token -> order |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
36 |
val mk_eof: Position.T -> token |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
37 |
val eof: token |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
38 |
val is_eof: token -> bool |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
39 |
val stopper: token Scan.stopper |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
40 |
val terminals: string list |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
41 |
val is_terminal: string -> bool |
67556 | 42 |
val get_terminal: string -> token option |
49821
d15fe10593ff
clarified output token markup (see also bc22daeed49e);
wenzelm
parents:
48992
diff
changeset
|
43 |
val literal_markup: string -> Markup.T |
44736 | 44 |
val report_of_token: token -> Position.report |
39510
d9f5f01faa1b
Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents:
39507
diff
changeset
|
45 |
val reported_token_range: Proof.context -> token -> string |
18 | 46 |
val valued_token: token -> bool |
55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
47 |
val implode_string: Symbol.symbol list -> string |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
48 |
val explode_string: string * Position.T -> Symbol_Pos.T list |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
49 |
val implode_str: Symbol.symbol list -> string |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
50 |
val explode_str: string * Position.T -> Symbol_Pos.T list |
30573 | 51 |
val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
52 |
val read_indexname: string -> indexname |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
53 |
val read_var: string -> term |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
54 |
val read_variable: string -> indexname option |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
55 |
val read_nat: string -> int option |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
56 |
val read_int: string -> int option |
58421 | 57 |
val read_num: string -> {radix: int, leading_zeros: int, value: int} |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
58 |
val read_float: string -> {mant: int, exp: int} |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
59 |
val mark_class: string -> string val unmark_class: string -> string |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
60 |
val mark_type: string -> string val unmark_type: string -> string |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
61 |
val mark_const: string -> string val unmark_const: string -> string |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
62 |
val mark_fixed: string -> string val unmark_fixed: string -> string |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
63 |
val unmark: |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
64 |
{case_class: string -> 'a, |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
65 |
case_type: string -> 'a, |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
66 |
case_const: string -> 'a, |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
67 |
case_fixed: string -> 'a, |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
68 |
case_default: string -> 'a} -> string -> 'a |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
69 |
val is_marked: string -> bool |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
70 |
val dummy_type: term |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
71 |
val fun_type: term |
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
72 |
end; |
0 | 73 |
|
14679 | 74 |
structure Lexicon: LEXICON = |
0 | 75 |
struct |
76 |
||
42476 | 77 |
(** syntaxtic terms **) |
78 |
||
79 |
structure Syntax = |
|
80 |
struct |
|
81 |
||
82 |
fun const c = Const (c, dummyT); |
|
83 |
fun free x = Free (x, dummyT); |
|
84 |
fun var xi = Var (xi, dummyT); |
|
85 |
||
86 |
end; |
|
87 |
||
88 |
||
89 |
||
4703 | 90 |
(** basic scanners **) |
91 |
||
30573 | 92 |
open Basic_Symbol_Pos; |
27773 | 93 |
|
55105 | 94 |
val err_prefix = "Inner lexical error: "; |
95 |
||
96 |
fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); |
|
27773 | 97 |
|
50239 | 98 |
val scan_id = Symbol_Pos.scan_ident; |
61476 | 99 |
val scan_longid = scan_id @@@ Scan.repeats1 ($$$ "." @@@ scan_id); |
27773 | 100 |
val scan_tid = $$$ "'" @@@ scan_id; |
4703 | 101 |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
102 |
val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); |
27773 | 103 |
val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1"); |
62782 | 104 |
val scan_num = scan_hex || scan_bin || Symbol_Pos.scan_nat; |
4703 | 105 |
|
62782 | 106 |
val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ Symbol_Pos.scan_nat) []; |
27773 | 107 |
val scan_var = $$$ "?" @@@ scan_id_nat; |
108 |
val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat; |
|
4703 | 109 |
|
50239 | 110 |
fun is_tid s = |
111 |
(case try (unprefix "'") s of |
|
112 |
SOME s' => Symbol_Pos.is_identifier s' |
|
113 |
| NONE => false); |
|
114 |
||
4703 | 115 |
|
116 |
||
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
117 |
(** tokens **) |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
118 |
|
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
119 |
(* datatype token_kind *) |
0 | 120 |
|
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
121 |
datatype token_kind = |
67548 | 122 |
Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str | |
67550 | 123 |
String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF; |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
124 |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
125 |
val token_kinds = |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
126 |
Vector.fromList |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
127 |
[Literal, Ident, Long_Ident, Var, Type_Ident, Type_Var, Num, Float, Str, |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
128 |
String, Cartouche, Space, Comment NONE, Comment (SOME Comment.Comment), |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
129 |
Comment (SOME Comment.Cancel), Comment (SOME Comment.Latex), Dummy, EOF]; |
67539 | 130 |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
131 |
fun token_kind i = Vector.sub (token_kinds, i); |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
132 |
fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds)); |
67539 | 133 |
|
134 |
||
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
135 |
(* datatype token *) |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
136 |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
137 |
datatype token = Token of int * string * Position.range; |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
138 |
|
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
139 |
fun index_of_token (Token (i, _, _)) = i; |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
140 |
val kind_of_token = index_of_token #> token_kind; |
27806 | 141 |
fun str_of_token (Token (_, s, _)) = s; |
142 |
fun pos_of_token (Token (_, _, (pos, _))) = pos; |
|
67551 | 143 |
fun end_pos_of_token (Token (_, _, (_, end_pos))) = end_pos; |
27806 | 144 |
|
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67413
diff
changeset
|
145 |
val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true); |
27887 | 146 |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
147 |
val dummy = Token (token_kind_index Dummy, "", Position.no_range); |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
148 |
|
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
149 |
|
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
150 |
(* literals *) |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
151 |
|
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
152 |
val literal_index = token_kind_index Literal; |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
153 |
fun literal s = Token (literal_index, s, Position.no_range); |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
154 |
fun is_literal tok = index_of_token tok = literal_index; |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
155 |
|
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
156 |
fun tokens_match_ord toks = |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
157 |
let val is = apply2 index_of_token toks in |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
158 |
(case int_ord is of |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
159 |
EQUAL => if #1 is = literal_index then fast_string_ord (apply2 str_of_token toks) else EQUAL |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
160 |
| ord => ord) |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
161 |
end; |
67550 | 162 |
|
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
163 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
164 |
(* stopper *) |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
165 |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
166 |
val eof_index = token_kind_index EOF; |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
167 |
fun mk_eof pos = Token (eof_index, "", (pos, Position.none)); |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
168 |
val eof = mk_eof Position.none; |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
169 |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
170 |
fun is_eof tok = index_of_token tok = eof_index; |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
171 |
val stopper = Scan.stopper (K eof) is_eof; |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
172 |
|
0 | 173 |
|
67556 | 174 |
(* terminal symbols *) |
0 | 175 |
|
67556 | 176 |
val terminal_symbols = |
177 |
[("id", Ident), |
|
178 |
("longid", Long_Ident), |
|
179 |
("var", Var), |
|
180 |
("tid", Type_Ident), |
|
181 |
("tvar", Type_Var), |
|
182 |
("num_token", Num), |
|
183 |
("float_token", Float), |
|
184 |
("str_token", Str), |
|
185 |
("string_token", String), |
|
186 |
("cartouche", Cartouche)] |
|
187 |
|> map (apsnd token_kind_index) |
|
188 |
|> Symtab.make; |
|
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
189 |
|
67556 | 190 |
val terminals = Symtab.keys terminal_symbols; |
191 |
val is_terminal = Symtab.defined terminal_symbols; |
|
192 |
fun get_terminal s = |
|
193 |
(case Symtab.lookup terminal_symbols s of |
|
194 |
SOME i => SOME (Token (i, s, Position.no_range)) |
|
195 |
| NONE => NONE); |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
196 |
|
0 | 197 |
|
27887 | 198 |
(* markup *) |
199 |
||
49821
d15fe10593ff
clarified output token markup (see also bc22daeed49e);
wenzelm
parents:
48992
diff
changeset
|
200 |
fun literal_markup s = |
52189 | 201 |
if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s) |
202 |
then Markup.literal |
|
203 |
else Markup.delimiter; |
|
49821
d15fe10593ff
clarified output token markup (see also bc22daeed49e);
wenzelm
parents:
48992
diff
changeset
|
204 |
|
27887 | 205 |
val token_kind_markup = |
67548 | 206 |
fn Type_Ident => Markup.tfree |
207 |
| Type_Var => Markup.tvar |
|
208 |
| Num => Markup.numeral |
|
209 |
| Float => Markup.numeral |
|
210 |
| Str => Markup.inner_string |
|
211 |
| String => Markup.inner_string |
|
55033 | 212 |
| Cartouche => Markup.inner_cartouche |
67440 | 213 |
| Comment _ => Markup.inner_comment |
55033 | 214 |
| _ => Markup.empty; |
27887 | 215 |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
216 |
fun report_of_token tok = |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
217 |
let |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
218 |
val markup = |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
219 |
if is_literal tok then literal_markup (str_of_token tok) |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
220 |
else token_kind_markup (kind_of_token tok); |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
221 |
in (pos_of_token tok, markup) end; |
27887 | 222 |
|
39510
d9f5f01faa1b
Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents:
39507
diff
changeset
|
223 |
fun reported_token_range ctxt tok = |
39168
e3ac771235f7
report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38474
diff
changeset
|
224 |
if is_proper tok |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49821
diff
changeset
|
225 |
then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range "" |
39510
d9f5f01faa1b
Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents:
39507
diff
changeset
|
226 |
else ""; |
39168
e3ac771235f7
report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38474
diff
changeset
|
227 |
|
27887 | 228 |
|
18 | 229 |
(* valued_token *) |
0 | 230 |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
231 |
fun valued_token tok = |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
232 |
not (is_literal tok orelse is_eof tok); |
0 | 233 |
|
234 |
||
55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
235 |
|
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
236 |
(** string literals **) |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
237 |
|
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
238 |
fun explode_literal scan_body (str, pos) = |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
239 |
(case Scan.read Symbol_Pos.stopper scan_body (Symbol_Pos.explode (str, pos)) of |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
240 |
SOME ss => ss |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
241 |
| _ => error (err_prefix ^ "malformed string literal " ^ quote str ^ Position.here pos)); |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
242 |
|
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
243 |
|
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
244 |
(* string *) |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
245 |
|
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
246 |
val scan_string = Scan.trace (Symbol_Pos.scan_string_qq err_prefix) >> #2; |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
247 |
val scan_string_body = Symbol_Pos.scan_string_qq err_prefix >> (#1 o #2); |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
248 |
|
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
249 |
fun implode_string ss = quote (implode (map (fn "\"" => "\\\"" | s => s) ss)); |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
250 |
val explode_string = explode_literal scan_string_body; |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
251 |
|
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
252 |
|
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
253 |
(* str *) |
18 | 254 |
|
14730 | 255 |
val scan_chr = |
55107 | 256 |
$$ "\\" |-- $$$ "'" || |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
257 |
Scan.one |
58854 | 258 |
((fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) o |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
259 |
Symbol_Pos.symbol) >> single || |
55107 | 260 |
$$$ "'" --| Scan.ahead (~$$ "'"); |
14730 | 261 |
|
262 |
val scan_str = |
|
55106 | 263 |
Scan.ahead ($$ "'" -- $$ "'") |-- |
264 |
!!! "unclosed string literal" |
|
61476 | 265 |
($$$ "'" @@@ $$$ "'" @@@ Scan.repeats scan_chr @@@ $$$ "'" @@@ $$$ "'"); |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
266 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
267 |
val scan_str_body = |
55107 | 268 |
Scan.ahead ($$ "'" |-- $$ "'") |-- |
55106 | 269 |
!!! "unclosed string literal" |
61476 | 270 |
($$ "'" |-- $$ "'" |-- Scan.repeats scan_chr --| $$ "'" --| $$ "'"); |
14730 | 271 |
|
55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
272 |
fun implode_str ss = enclose "''" "''" (implode (map (fn "'" => "\\'" | s => s) ss)); |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
273 |
val explode_str = explode_literal scan_str_body; |
18 | 274 |
|
275 |
||
27806 | 276 |
|
18 | 277 |
(** tokenize **) |
278 |
||
67412 | 279 |
val token_leq = op <= o apply2 str_of_token; |
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
280 |
|
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
281 |
fun token kind = |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
282 |
let val i = token_kind_index kind |
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
283 |
in fn ss => Token (i, Symbol_Pos.content ss, Symbol_Pos.range ss) end; |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
284 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
285 |
fun tokenize lex xids syms = |
18 | 286 |
let |
287 |
val scan_xid = |
|
55962
fbd0e768bc8f
special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
wenzelm
parents:
55624
diff
changeset
|
288 |
(if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) || |
fbd0e768bc8f
special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
wenzelm
parents:
55624
diff
changeset
|
289 |
$$$ "_" @@@ $$$ "_"; |
18 | 290 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
291 |
val scan_val = |
67548 | 292 |
scan_tvar >> token Type_Var || |
293 |
scan_var >> token Var || |
|
294 |
scan_tid >> token Type_Ident || |
|
295 |
Symbol_Pos.scan_float >> token Float || |
|
296 |
scan_num >> token Num || |
|
297 |
scan_longid >> token Long_Ident || |
|
298 |
scan_xid >> token Ident; |
|
18 | 299 |
|
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
300 |
val scan_lit = Scan.literal lex >> token Literal; |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
301 |
|
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
302 |
val scan = |
55105 | 303 |
Symbol_Pos.scan_cartouche err_prefix >> token Cartouche || |
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67413
diff
changeset
|
304 |
Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) || |
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67413
diff
changeset
|
305 |
Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) || |
27887 | 306 |
Scan.max token_leq scan_lit scan_val || |
67548 | 307 |
scan_string >> token String || |
308 |
scan_str >> token Str || |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
309 |
Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space; |
18 | 310 |
in |
67555
c550e38dd131
more efficient tokens_match_ord based on token_kind_index;
wenzelm
parents:
67554
diff
changeset
|
311 |
(case Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan)) syms of |
27887 | 312 |
(toks, []) => toks |
55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55107
diff
changeset
|
313 |
| (_, ss) => |
55624 | 314 |
error ("Inner lexical error" ^ Position.here (#1 (Symbol_Pos.range ss)) ^ |
315 |
Markup.markup Markup.no_report ("\nat " ^ quote (Symbol_Pos.content ss)))) |
|
18 | 316 |
end; |
317 |
||
318 |
||
319 |
||
320 |
(** scan variables **) |
|
321 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
322 |
(* scan_indexname *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
323 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
324 |
local |
18 | 325 |
|
27773 | 326 |
val scan_vname = |
18 | 327 |
let |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
328 |
fun nat n [] = n |
64275
ac2abc987cf9
accomodate Poly/ML repository version, which treats singleton strings as boxed;
wenzelm
parents:
62819
diff
changeset
|
329 |
| nat n (c :: cs) = nat (n * 10 + (ord c - Char.ord #"0")) cs; |
18 | 330 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
331 |
fun idxname cs ds = (implode (rev cs), nat 0 ds); |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
332 |
fun chop_idx [] ds = idxname [] ds |
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61476
diff
changeset
|
333 |
| chop_idx (cs as (_ :: "\<^sub>" :: _)) ds = idxname cs ds |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
334 |
| chop_idx (c :: cs) ds = |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
335 |
if Symbol.is_digit c then chop_idx cs (c :: ds) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
336 |
else idxname (c :: cs) ds; |
18 | 337 |
|
50239 | 338 |
val scan = |
339 |
(scan_id >> map Symbol_Pos.symbol) -- |
|
62782 | 340 |
Scan.optional ($$ "." |-- Symbol_Pos.scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1; |
18 | 341 |
in |
27773 | 342 |
scan >> |
343 |
(fn (cs, ~1) => chop_idx (rev cs) [] |
|
344 |
| (cs, i) => (implode cs, i)) |
|
18 | 345 |
end; |
346 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
347 |
in |
18 | 348 |
|
55107 | 349 |
val scan_indexname = $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname; |
15443
07f78cc82a73
indexname function now parses type variables as well; changed input
berghofe
parents:
14981
diff
changeset
|
350 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
351 |
end; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
352 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
353 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
354 |
(* indexname *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
355 |
|
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
356 |
fun read_indexname s = |
62751 | 357 |
(case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode0 s) of |
15531 | 358 |
SOME xi => xi |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
359 |
| _ => error ("Lexical error in variable name: " ^ quote s)); |
18 | 360 |
|
361 |
||
4703 | 362 |
(* read_var *) |
18 | 363 |
|
4703 | 364 |
fun read_var str = |
18 | 365 |
let |
366 |
val scan = |
|
55107 | 367 |
$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) |
42476 | 368 |
>> Syntax.var || |
58854 | 369 |
Scan.many (Symbol.not_eof o Symbol_Pos.symbol) |
42476 | 370 |
>> (Syntax.free o implode o map Symbol_Pos.symbol); |
62751 | 371 |
in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str)) end; |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
372 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
373 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
374 |
(* read_variable *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
375 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
376 |
fun read_variable str = |
55107 | 377 |
let val scan = $$ "?" |-- scan_indexname || scan_indexname |
62751 | 378 |
in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str) end; |
4587 | 379 |
|
380 |
||
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
381 |
(* read numbers *) |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
382 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
383 |
local |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
384 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
385 |
fun nat cs = |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
386 |
Option.map (#1 o Library.read_int o map Symbol_Pos.symbol) |
62782 | 387 |
(Scan.read Symbol_Pos.stopper Symbol_Pos.scan_nat cs); |
5860 | 388 |
|
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
389 |
in |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
390 |
|
62751 | 391 |
fun read_nat s = nat (Symbol_Pos.explode0 s); |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
392 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
393 |
fun read_int s = |
62751 | 394 |
(case Symbol_Pos.explode0 s of |
27773 | 395 |
("-", _) :: cs => Option.map ~ (nat cs) |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
396 |
| cs => nat cs); |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
397 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
398 |
end; |
5860 | 399 |
|
400 |
||
58421 | 401 |
(* read_num: hex/bin/decimal *) |
9326 | 402 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
403 |
local |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
404 |
|
64275
ac2abc987cf9
accomodate Poly/ML repository version, which treats singleton strings as boxed;
wenzelm
parents:
62819
diff
changeset
|
405 |
val ten = Char.ord #"0" + 10; |
ac2abc987cf9
accomodate Poly/ML repository version, which treats singleton strings as boxed;
wenzelm
parents:
62819
diff
changeset
|
406 |
val a = Char.ord #"a"; |
ac2abc987cf9
accomodate Poly/ML repository version, which treats singleton strings as boxed;
wenzelm
parents:
62819
diff
changeset
|
407 |
val A = Char.ord #"A"; |
35428 | 408 |
val _ = a > A orelse raise Fail "Bad ASCII"; |
20096 | 409 |
|
410 |
fun remap_hex c = |
|
411 |
let val x = ord c in |
|
412 |
if x >= a then chr (x - a + ten) |
|
413 |
else if x >= A then chr (x - A + ten) |
|
414 |
else c |
|
415 |
end; |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
416 |
|
21781 | 417 |
fun leading_zeros ["0"] = 0 |
418 |
| leading_zeros ("0" :: cs) = 1 + leading_zeros cs |
|
419 |
| leading_zeros _ = 0; |
|
420 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
421 |
in |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
422 |
|
58421 | 423 |
fun read_num str = |
9326 | 424 |
let |
58421 | 425 |
val (radix, digs) = |
426 |
(case Symbol.explode str of |
|
427 |
"0" :: "x" :: cs => (16, map remap_hex cs) |
|
428 |
| "0" :: "b" :: cs => (2, cs) |
|
429 |
| cs => (10, cs)); |
|
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
430 |
in |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
431 |
{radix = radix, |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
432 |
leading_zeros = leading_zeros digs, |
58421 | 433 |
value = #1 (Library.read_radix_int radix digs)} |
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
434 |
end; |
9326 | 435 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
436 |
end; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
437 |
|
28904 | 438 |
fun read_float str = |
439 |
let |
|
58421 | 440 |
val cs = Symbol.explode str; |
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
441 |
val (intpart, fracpart) = |
67522 | 442 |
(case chop_prefix Symbol.is_digit cs of |
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
443 |
(intpart, "." :: fracpart) => (intpart, fracpart) |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
444 |
| _ => raise Fail "read_float"); |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
445 |
in |
58421 | 446 |
{mant = #1 (Library.read_int (intpart @ fracpart)), |
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
447 |
exp = length fracpart} |
42046
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
448 |
end; |
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
449 |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
450 |
|
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
451 |
(* marked logical entities *) |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
452 |
|
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
453 |
fun marker s = (prefix s, unprefix s); |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
454 |
|
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61476
diff
changeset
|
455 |
val (mark_class, unmark_class) = marker "\<^class>"; |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61476
diff
changeset
|
456 |
val (mark_type, unmark_type) = marker "\<^type>"; |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61476
diff
changeset
|
457 |
val (mark_const, unmark_const) = marker "\<^const>"; |
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
61476
diff
changeset
|
458 |
val (mark_fixed, unmark_fixed) = marker "\<^fixed>"; |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
459 |
|
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
460 |
fun unmark {case_class, case_type, case_const, case_fixed, case_default} s = |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
461 |
(case try unmark_class s of |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
462 |
SOME c => case_class c |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
463 |
| NONE => |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
464 |
(case try unmark_type s of |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
465 |
SOME c => case_type c |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
466 |
| NONE => |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
467 |
(case try unmark_const s of |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
468 |
SOME c => case_const c |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
469 |
| NONE => |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
470 |
(case try unmark_fixed s of |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
471 |
SOME c => case_fixed c |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
472 |
| NONE => case_default s)))); |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
473 |
|
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
474 |
val is_marked = |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
475 |
unmark {case_class = K true, case_type = K true, case_const = K true, |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
476 |
case_fixed = K true, case_default = K false}; |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
477 |
|
42476 | 478 |
val dummy_type = Syntax.const (mark_type "dummy"); |
479 |
val fun_type = Syntax.const (mark_type "fun"); |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42264
diff
changeset
|
480 |
|
59196 | 481 |
|
482 |
(* toplevel pretty printing *) |
|
483 |
||
62663 | 484 |
val _ = |
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62782
diff
changeset
|
485 |
ML_system_pp (fn _ => fn _ => |
62663 | 486 |
Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon); |
59196 | 487 |
|
0 | 488 |
end; |