author | wenzelm |
Tue, 22 Mar 2011 16:15:50 +0100 | |
changeset 42053 | 006095137a81 |
parent 42048 | afd11ca8e018 |
child 42264 | b6c1b0c4c511 |
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 |
|
7 |
signature LEXICON0 = |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
8 |
sig |
0 | 9 |
val is_identifier: string -> bool |
14679 | 10 |
val is_ascii_identifier: string -> bool |
20165 | 11 |
val is_tid: string -> bool |
30573 | 12 |
val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
13 |
val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
|
14 |
val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
|
15 |
val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
|
16 |
val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
|
40290
47f572aff50a
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
39510
diff
changeset
|
17 |
val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
30573 | 18 |
val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
19 |
val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
|
20 |
val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
|
21 |
val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
22 |
val implode_xstr: string list -> string |
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
23 |
val explode_xstr: string -> string list |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
24 |
val read_indexname: string -> indexname |
4703 | 25 |
val read_var: string -> term |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
26 |
val read_variable: string -> indexname option |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
27 |
val const: string -> term |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
28 |
val free: string -> term |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
29 |
val var: indexname -> term |
5860 | 30 |
val read_nat: string -> int option |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
31 |
val read_int: string -> int option |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24583
diff
changeset
|
32 |
val read_xnum: string -> {radix: int, leading_zeros: int, value: int} |
28904 | 33 |
val read_float: string -> {mant: int, exp: int} |
35428 | 34 |
val mark_class: string -> string val unmark_class: string -> string |
35 |
val mark_type: string -> string val unmark_type: string -> string |
|
36 |
val mark_const: string -> string val unmark_const: string -> string |
|
37 |
val mark_fixed: string -> string val unmark_fixed: string -> string |
|
38 |
val unmark: |
|
39 |
{case_class: string -> 'a, |
|
40 |
case_type: string -> 'a, |
|
41 |
case_const: string -> 'a, |
|
42 |
case_fixed: string -> 'a, |
|
43 |
case_default: string -> 'a} -> string -> 'a |
|
44 |
val is_marked: string -> bool |
|
42053
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
42048
diff
changeset
|
45 |
val dummy_type: term |
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
42048
diff
changeset
|
46 |
val fun_type: term |
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
47 |
val pretty_position: Position.T -> Pretty.T |
42046
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
48 |
val encode_position: Position.T -> string |
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
49 |
val decode_position: string -> Position.T option |
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
50 |
end; |
0 | 51 |
|
52 |
signature LEXICON = |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
53 |
sig |
18 | 54 |
include LEXICON0 |
55 |
val is_xid: string -> bool |
|
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
56 |
datatype token_kind = |
27887 | 57 |
Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | |
28904 | 58 |
NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
59 |
datatype token = Token of token_kind * string * Position.range |
27806 | 60 |
val str_of_token: token -> string |
61 |
val pos_of_token: token -> Position.T |
|
27887 | 62 |
val is_proper: token -> bool |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
63 |
val mk_eof: Position.T -> token |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
64 |
val eof: token |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
65 |
val is_eof: token -> bool |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
66 |
val stopper: token Scan.stopper |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
67 |
val idT: typ |
3828 | 68 |
val longidT: typ |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
69 |
val varT: typ |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
70 |
val tidT: typ |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
71 |
val tvarT: typ |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
72 |
val terminals: string list |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
73 |
val is_terminal: string -> bool |
38237
8b0383334031
prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
wenzelm
parents:
35428
diff
changeset
|
74 |
val report_token: Proof.context -> token -> unit |
39510
d9f5f01faa1b
Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents:
39507
diff
changeset
|
75 |
val reported_token_range: Proof.context -> token -> string |
18 | 76 |
val matching_tokens: token * token -> bool |
77 |
val valued_token: token -> bool |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
78 |
val predef_term: string -> token option |
30573 | 79 |
val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list |
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
80 |
end; |
0 | 81 |
|
14679 | 82 |
structure Lexicon: LEXICON = |
0 | 83 |
struct |
84 |
||
18 | 85 |
(** is_identifier etc. **) |
86 |
||
16150 | 87 |
val is_identifier = Symbol.is_ident o Symbol.explode; |
18 | 88 |
|
14679 | 89 |
fun is_ascii_identifier s = |
90 |
let val cs = Symbol.explode s |
|
16150 | 91 |
in forall Symbol.is_ascii cs andalso Symbol.is_ident cs end; |
14679 | 92 |
|
18 | 93 |
fun is_xid s = |
4703 | 94 |
(case Symbol.explode s of |
16150 | 95 |
"_" :: cs => Symbol.is_ident cs |
96 |
| cs => Symbol.is_ident cs); |
|
18 | 97 |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
98 |
fun is_tid s = |
4703 | 99 |
(case Symbol.explode s of |
16150 | 100 |
"'" :: cs => Symbol.is_ident cs |
18 | 101 |
| _ => false); |
102 |
||
0 | 103 |
|
104 |
||
4703 | 105 |
(** basic scanners **) |
106 |
||
30573 | 107 |
open Basic_Symbol_Pos; |
27773 | 108 |
|
30573 | 109 |
fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg); |
27773 | 110 |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
111 |
val scan_id = |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
112 |
Scan.one (Symbol.is_letter o Symbol_Pos.symbol) ::: |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
113 |
Scan.many (Symbol.is_letdig o Symbol_Pos.symbol); |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
114 |
|
27773 | 115 |
val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat); |
116 |
val scan_tid = $$$ "'" @@@ scan_id; |
|
4703 | 117 |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
118 |
val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol); |
27773 | 119 |
val scan_int = $$$ "-" @@@ scan_nat || scan_nat; |
28904 | 120 |
val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat; |
121 |
val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot; |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
122 |
val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); |
27773 | 123 |
val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1"); |
4703 | 124 |
|
27773 | 125 |
val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) []; |
126 |
val scan_var = $$$ "?" @@@ scan_id_nat; |
|
127 |
val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat; |
|
4703 | 128 |
|
129 |
||
130 |
||
18 | 131 |
(** datatype token **) |
0 | 132 |
|
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
133 |
datatype token_kind = |
27887 | 134 |
Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | |
28904 | 135 |
NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF; |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
136 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
137 |
datatype token = Token of token_kind * string * Position.range; |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
138 |
|
27806 | 139 |
fun str_of_token (Token (_, s, _)) = s; |
140 |
fun pos_of_token (Token (_, _, (pos, _))) = pos; |
|
141 |
||
27887 | 142 |
fun is_proper (Token (Space, _, _)) = false |
143 |
| is_proper (Token (Comment, _, _)) = false |
|
144 |
| is_proper _ = true; |
|
145 |
||
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
146 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
147 |
(* stopper *) |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
148 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
149 |
fun mk_eof pos = Token (EOF, "", (pos, Position.none)); |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
150 |
val eof = mk_eof Position.none; |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
151 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
152 |
fun is_eof (Token (EOF, _, _)) = true |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
153 |
| is_eof _ = false; |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
154 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
155 |
val stopper = Scan.stopper (K eof) is_eof; |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
156 |
|
0 | 157 |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
158 |
(* terminal arguments *) |
0 | 159 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
160 |
val idT = Type ("id", []); |
3828 | 161 |
val longidT = Type ("longid", []); |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
162 |
val varT = Type ("var", []); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
163 |
val tidT = Type ("tid", []); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
164 |
val tvarT = Type ("tvar", []); |
0 | 165 |
|
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
166 |
val terminal_kinds = |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
167 |
[("id", IdentSy), |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
168 |
("longid", LongIdentSy), |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
169 |
("var", VarSy), |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
170 |
("tid", TFreeSy), |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
171 |
("tvar", TVarSy), |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
172 |
("num", NumSy), |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
173 |
("float_token", FloatSy), |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
174 |
("xnum", XNumSy), |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
175 |
("xstr", StrSy)]; |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
176 |
|
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
177 |
val terminals = map #1 terminal_kinds; |
20664 | 178 |
val is_terminal = member (op =) terminals; |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
179 |
|
0 | 180 |
|
27887 | 181 |
(* markup *) |
182 |
||
183 |
val token_kind_markup = |
|
184 |
fn Literal => Markup.literal |
|
185 |
| IdentSy => Markup.ident |
|
186 |
| LongIdentSy => Markup.ident |
|
187 |
| VarSy => Markup.var |
|
188 |
| TFreeSy => Markup.tfree |
|
189 |
| TVarSy => Markup.tvar |
|
29318
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
29156
diff
changeset
|
190 |
| NumSy => Markup.numeral |
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
29156
diff
changeset
|
191 |
| FloatSy => Markup.numeral |
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
29156
diff
changeset
|
192 |
| XNumSy => Markup.numeral |
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
29156
diff
changeset
|
193 |
| StrSy => Markup.inner_string |
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38237
diff
changeset
|
194 |
| Space => Markup.empty |
27887 | 195 |
| Comment => Markup.inner_comment |
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38237
diff
changeset
|
196 |
| EOF => Markup.empty; |
27887 | 197 |
|
38237
8b0383334031
prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
wenzelm
parents:
35428
diff
changeset
|
198 |
fun report_token ctxt (Token (kind, _, (pos, _))) = |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39168
diff
changeset
|
199 |
Context_Position.report ctxt pos (token_kind_markup kind); |
27887 | 200 |
|
39510
d9f5f01faa1b
Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents:
39507
diff
changeset
|
201 |
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
|
202 |
if is_proper tok |
39510
d9f5f01faa1b
Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents:
39507
diff
changeset
|
203 |
then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range "" |
d9f5f01faa1b
Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents:
39507
diff
changeset
|
204 |
else ""; |
39168
e3ac771235f7
report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38474
diff
changeset
|
205 |
|
27887 | 206 |
|
18 | 207 |
(* matching_tokens *) |
0 | 208 |
|
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
209 |
fun matching_tokens (Token (Literal, x, _), Token (Literal, y, _)) = x = y |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
210 |
| matching_tokens (Token (k, _, _), Token (k', _, _)) = k = k'; |
0 | 211 |
|
212 |
||
18 | 213 |
(* valued_token *) |
0 | 214 |
|
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
215 |
fun valued_token (Token (Literal, _, _)) = false |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
216 |
| valued_token (Token (EOF, _, _)) = false |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
217 |
| valued_token _ = true; |
0 | 218 |
|
219 |
||
18 | 220 |
(* predef_term *) |
0 | 221 |
|
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
222 |
fun predef_term s = |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
223 |
(case AList.lookup (op =) terminal_kinds s of |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
224 |
SOME sy => SOME (Token (sy, s, Position.no_range)) |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
225 |
| NONE => NONE); |
0 | 226 |
|
227 |
||
4703 | 228 |
(* xstr tokens *) |
18 | 229 |
|
14730 | 230 |
val scan_chr = |
27773 | 231 |
$$$ "\\" |-- $$$ "'" || |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
232 |
Scan.one |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
233 |
((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
234 |
Symbol_Pos.symbol) >> single || |
27773 | 235 |
$$$ "'" --| Scan.ahead (~$$$ "'"); |
14730 | 236 |
|
237 |
val scan_str = |
|
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
238 |
$$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string" |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
239 |
((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'"); |
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
240 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
241 |
val scan_str_body = |
27773 | 242 |
$$$ "'" |-- $$$ "'" |-- !!! "missing end of string" |
243 |
((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'"); |
|
14730 | 244 |
|
0 | 245 |
|
4703 | 246 |
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs)); |
18 | 247 |
|
4703 | 248 |
fun explode_xstr str = |
30573 | 249 |
(case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
250 |
SOME cs => map Symbol_Pos.symbol cs |
5868 | 251 |
| _ => error ("Inner lexical error: literal string expected at " ^ quote str)); |
18 | 252 |
|
253 |
||
27806 | 254 |
|
18 | 255 |
(** tokenize **) |
256 |
||
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
257 |
fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2; |
30573 | 258 |
fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss); |
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
259 |
|
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
260 |
fun tokenize lex xids syms = |
18 | 261 |
let |
262 |
val scan_xid = |
|
27773 | 263 |
if xids then $$$ "_" @@@ scan_id || scan_id |
18 | 264 |
else scan_id; |
265 |
||
20096 | 266 |
val scan_num = scan_hex || scan_bin || scan_int; |
267 |
||
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
268 |
val scan_val = |
26007
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
269 |
scan_tvar >> token TVarSy || |
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
270 |
scan_var >> token VarSy || |
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
271 |
scan_tid >> token TFreeSy || |
28904 | 272 |
scan_float >> token FloatSy || |
26007
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
273 |
scan_num >> token NumSy || |
27773 | 274 |
$$$ "#" @@@ scan_num >> token XNumSy || |
26007
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
275 |
scan_longid >> token LongIdentSy || |
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
276 |
scan_xid >> token IdentSy; |
18 | 277 |
|
27800
df444ddeff56
datatype token: maintain range, tuned representation;
wenzelm
parents:
27773
diff
changeset
|
278 |
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
|
279 |
|
4703 | 280 |
val scan_token = |
30573 | 281 |
Symbol_Pos.scan_comment !!! >> token Comment || |
27887 | 282 |
Scan.max token_leq scan_lit scan_val || |
283 |
scan_str >> token StrSy || |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
284 |
Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space; |
18 | 285 |
in |
27773 | 286 |
(case Scan.error |
30573 | 287 |
(Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of |
27887 | 288 |
(toks, []) => toks |
30573 | 289 |
| (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^ |
290 |
Position.str_of (#1 (Symbol_Pos.range ss)))) |
|
18 | 291 |
end; |
292 |
||
293 |
||
294 |
||
295 |
(** scan variables **) |
|
296 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
297 |
(* scan_indexname *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
298 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
299 |
local |
18 | 300 |
|
27773 | 301 |
val scan_vname = |
18 | 302 |
let |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
303 |
fun nat n [] = n |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
304 |
| nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs; |
18 | 305 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
306 |
fun idxname cs ds = (implode (rev cs), nat 0 ds); |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
307 |
fun chop_idx [] ds = idxname [] ds |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
308 |
| chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
309 |
| chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
310 |
| chop_idx (c :: cs) ds = |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
311 |
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
|
312 |
else idxname (c :: cs) ds; |
18 | 313 |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
314 |
val scan = (scan_id >> map Symbol_Pos.symbol) -- |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
315 |
Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1; |
18 | 316 |
in |
27773 | 317 |
scan >> |
318 |
(fn (cs, ~1) => chop_idx (rev cs) [] |
|
319 |
| (cs, i) => (implode cs, i)) |
|
18 | 320 |
end; |
321 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
322 |
in |
18 | 323 |
|
27773 | 324 |
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
|
325 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
326 |
end; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
327 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
328 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
329 |
(* indexname *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
330 |
|
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
331 |
fun read_indexname s = |
30573 | 332 |
(case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of |
15531 | 333 |
SOME xi => xi |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
334 |
| _ => error ("Lexical error in variable name: " ^ quote s)); |
18 | 335 |
|
336 |
||
4703 | 337 |
(* read_var *) |
18 | 338 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
339 |
fun const c = Const (c, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
340 |
fun free x = Free (x, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
341 |
fun var xi = Var (xi, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
342 |
|
4703 | 343 |
fun read_var str = |
18 | 344 |
let |
345 |
val scan = |
|
30573 | 346 |
$$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var || |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
347 |
Scan.many (Symbol.is_regular o Symbol_Pos.symbol) >> (free o implode o map Symbol_Pos.symbol); |
30573 | 348 |
in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end; |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
349 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
350 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
351 |
(* read_variable *) |
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 |
fun read_variable str = |
27773 | 354 |
let val scan = $$$ "?" |-- scan_indexname || scan_indexname |
30573 | 355 |
in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end; |
4587 | 356 |
|
357 |
||
35428 | 358 |
(* logical entities *) |
359 |
||
360 |
fun marker s = (prefix s, unprefix s); |
|
361 |
||
362 |
val (mark_class, unmark_class) = marker "\\<^class>"; |
|
363 |
val (mark_type, unmark_type) = marker "\\<^type>"; |
|
364 |
val (mark_const, unmark_const) = marker "\\<^const>"; |
|
365 |
val (mark_fixed, unmark_fixed) = marker "\\<^fixed>"; |
|
5260 | 366 |
|
35428 | 367 |
fun unmark {case_class, case_type, case_const, case_fixed, case_default} s = |
368 |
(case try unmark_class s of |
|
369 |
SOME c => case_class c |
|
370 |
| NONE => |
|
371 |
(case try unmark_type s of |
|
372 |
SOME c => case_type c |
|
373 |
| NONE => |
|
374 |
(case try unmark_const s of |
|
375 |
SOME c => case_const c |
|
376 |
| NONE => |
|
377 |
(case try unmark_fixed s of |
|
378 |
SOME c => case_fixed c |
|
379 |
| NONE => case_default s)))); |
|
35262
9ea4445d2ccf
slightly more abstract syntax mark/unmark operations;
wenzelm
parents:
30573
diff
changeset
|
380 |
|
35428 | 381 |
val is_marked = |
382 |
unmark {case_class = K true, case_type = K true, case_const = K true, |
|
383 |
case_fixed = K true, case_default = K false}; |
|
19002 | 384 |
|
42053
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
42048
diff
changeset
|
385 |
val dummy_type = const (mark_type "dummy"); |
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
42048
diff
changeset
|
386 |
val fun_type = const (mark_type "fun"); |
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
42048
diff
changeset
|
387 |
|
5260 | 388 |
|
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
389 |
(* read numbers *) |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
390 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
391 |
local |
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 nat cs = |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40290
diff
changeset
|
394 |
Option.map (#1 o Library.read_int o map Symbol_Pos.symbol) |
30573 | 395 |
(Scan.read Symbol_Pos.stopper scan_nat cs); |
5860 | 396 |
|
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
397 |
in |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
398 |
|
30573 | 399 |
fun read_nat s = nat (Symbol_Pos.explode (s, Position.none)); |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
400 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
401 |
fun read_int s = |
30573 | 402 |
(case Symbol_Pos.explode (s, Position.none) of |
27773 | 403 |
("-", _) :: cs => Option.map ~ (nat cs) |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
404 |
| cs => nat cs); |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
405 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
406 |
end; |
5860 | 407 |
|
408 |
||
20096 | 409 |
(* read_xnum: hex/bin/decimal *) |
9326 | 410 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
411 |
local |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
412 |
|
20096 | 413 |
val ten = ord "0" + 10; |
414 |
val a = ord "a"; |
|
415 |
val A = ord "A"; |
|
35428 | 416 |
val _ = a > A orelse raise Fail "Bad ASCII"; |
20096 | 417 |
|
418 |
fun remap_hex c = |
|
419 |
let val x = ord c in |
|
420 |
if x >= a then chr (x - a + ten) |
|
421 |
else if x >= A then chr (x - A + ten) |
|
422 |
else c |
|
423 |
end; |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
424 |
|
21781 | 425 |
fun leading_zeros ["0"] = 0 |
426 |
| leading_zeros ("0" :: cs) = 1 + leading_zeros cs |
|
427 |
| leading_zeros _ = 0; |
|
428 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
429 |
in |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
430 |
|
9326 | 431 |
fun read_xnum str = |
432 |
let |
|
20096 | 433 |
val (sign, radix, digs) = |
434 |
(case Symbol.explode (perhaps (try (unprefix "#")) str) of |
|
435 |
"0" :: "x" :: cs => (1, 16, map remap_hex cs) |
|
436 |
| "0" :: "b" :: cs => (1, 2, cs) |
|
437 |
| "-" :: cs => (~1, 10, cs) |
|
438 |
| cs => (1, 10, cs)); |
|
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
439 |
in |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
440 |
{radix = radix, |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
441 |
leading_zeros = leading_zeros digs, |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
442 |
value = sign * #1 (Library.read_radix_int radix digs)} |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
443 |
end; |
9326 | 444 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
445 |
end; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
446 |
|
28904 | 447 |
fun read_float str = |
448 |
let |
|
449 |
val (sign, cs) = |
|
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
450 |
(case Symbol.explode str of |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
451 |
"-" :: cs => (~1, cs) |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
452 |
| cs => (1, cs)); |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
453 |
val (intpart, fracpart) = |
28904 | 454 |
(case take_prefix Symbol.is_digit cs of |
29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
455 |
(intpart, "." :: fracpart) => (intpart, fracpart) |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
456 |
| _ => raise Fail "read_float"); |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
457 |
in |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
458 |
{mant = sign * #1 (Library.read_int (intpart @ fracpart)), |
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
28904
diff
changeset
|
459 |
exp = length fracpart} |
42046
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
460 |
end; |
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
461 |
|
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
462 |
|
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
463 |
(* positions *) |
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
464 |
|
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
465 |
val position_dummy = "<position>"; |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
466 |
val position_text = XML.Text position_dummy; |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
467 |
|
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
468 |
fun pretty_position pos = |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
469 |
Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy]; |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
470 |
|
42046
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
471 |
fun encode_position pos = |
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
472 |
YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text])); |
42046
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
473 |
|
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
474 |
fun decode_position str = |
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
475 |
(case YXML.parse_body str handle Fail msg => error msg of |
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
476 |
[XML.Elem ((name, props), [arg])] => |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
477 |
if name = Markup.positionN andalso arg = position_text |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
42046
diff
changeset
|
478 |
then SOME (Position.of_properties props) |
42046
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
479 |
else NONE |
6341c23baf10
added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents:
40525
diff
changeset
|
480 |
| _ => NONE); |
28904 | 481 |
|
0 | 482 |
end; |