author | wenzelm |
Tue, 25 Feb 2014 17:23:20 +0100 | |
changeset 55745 | b865c3035d5c |
parent 55744 | 4a4e5686e091 |
child 55750 | baa7a1e57f4a |
permissions | -rw-r--r-- |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
1 |
(* Title: Pure/Isar/token.ML |
5825 | 2 |
Author: Markus Wenzel, TU Muenchen |
3 |
||
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
4 |
Outer token syntax for Isabelle/Isar. |
5825 | 5 |
*) |
6 |
||
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
7 |
signature TOKEN = |
5825 | 8 |
sig |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
9 |
datatype kind = |
27814 | 10 |
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | |
55033 | 11 |
Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue | |
40958
755f8fe7ced9
eliminated obsolete Token.Malformed -- subsumed by Token.Error;
wenzelm
parents:
40627
diff
changeset
|
12 |
Error of string | Sync | EOF |
48905 | 13 |
type file = {src_path: Path.T, text: string, pos: Position.T} |
27814 | 14 |
datatype value = |
15 |
Text of string | Typ of typ | Term of term | Fact of thm list | |
|
54520
cee77d2e9582
release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents:
54519
diff
changeset
|
16 |
Attribute of morphism -> attribute | Files of file Exn.result list |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
17 |
type T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
18 |
val str_of_kind: kind -> string |
55708 | 19 |
val pos_of: T -> Position.T |
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
20 |
val range_of: T list -> Position.range |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
21 |
val eof: T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
22 |
val is_eof: T -> bool |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
23 |
val not_eof: T -> bool |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
24 |
val not_sync: T -> bool |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
25 |
val stopper: T Scan.stopper |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
26 |
val kind_of: T -> kind |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
27 |
val is_kind: kind -> T -> bool |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
28 |
val keyword_with: (string -> bool) -> T -> bool |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
29 |
val ident_with: (string -> bool) -> T -> bool |
46811
03a2dc9e0624
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents:
45666
diff
changeset
|
30 |
val is_command: T -> bool |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
31 |
val is_name: T -> bool |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
32 |
val is_proper: T -> bool |
51266
3007d0bc9cb1
unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents:
50239
diff
changeset
|
33 |
val is_improper: T -> bool |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
34 |
val is_semicolon: T -> bool |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
35 |
val is_comment: T -> bool |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
36 |
val is_begin_ignore: T -> bool |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
37 |
val is_end_ignore: T -> bool |
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48743
diff
changeset
|
38 |
val is_error: T -> bool |
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset
|
39 |
val is_space: T -> bool |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
40 |
val is_blank: T -> bool |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
41 |
val is_newline: T -> bool |
55111 | 42 |
val inner_syntax_of: T -> string |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
43 |
val source_position_of: T -> Symbol_Pos.text * Position.T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
44 |
val content_of: T -> string |
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
45 |
val markup: T -> Markup.T * string |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
46 |
val unparse: T -> string |
55745 | 47 |
val print: T -> string |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
48 |
val text_of: T -> string * string |
54520
cee77d2e9582
release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents:
54519
diff
changeset
|
49 |
val get_files: T -> file Exn.result list |
cee77d2e9582
release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents:
54519
diff
changeset
|
50 |
val put_files: file Exn.result list -> T -> T |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
51 |
val get_value: T -> value option |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
52 |
val map_value: (value -> value) -> T -> T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
53 |
val mk_text: string -> T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
54 |
val mk_typ: typ -> T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
55 |
val mk_term: term -> T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
56 |
val mk_fact: thm list -> T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
57 |
val mk_attribute: (morphism -> attribute) -> T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
58 |
val assignable: T -> T |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
59 |
val assign: value option -> T -> unit |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
60 |
val closure: T -> T |
27814 | 61 |
val ident_or_symbolic: string -> bool |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
62 |
val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source |
48741 | 63 |
val source': {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) -> |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
64 |
(Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source |
48741 | 65 |
val source: {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) -> |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
66 |
Position.T -> (Symbol.symbol, 'a) Source.source -> (T, |
30573 | 67 |
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
68 |
val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a |
5825 | 69 |
end; |
70 |
||
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
71 |
structure Token: TOKEN = |
5825 | 72 |
struct |
73 |
||
74 |
(** tokens **) |
|
75 |
||
27814 | 76 |
(* token values *) |
77 |
||
78 |
(*The value slot assigns an (optional) internal value to a token, |
|
79 |
usually as a side-effect of special scanner setup (see also |
|
80 |
args.ML). Note that an assignable ref designates an intermediate |
|
81 |
state of internalization -- it is NOT meant to persist.*) |
|
82 |
||
48905 | 83 |
type file = {src_path: Path.T, text: string, pos: Position.T}; |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
84 |
|
27814 | 85 |
datatype value = |
86 |
Text of string | |
|
87 |
Typ of typ | |
|
88 |
Term of term | |
|
89 |
Fact of thm list | |
|
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
90 |
Attribute of morphism -> attribute | |
54520
cee77d2e9582
release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents:
54519
diff
changeset
|
91 |
Files of file Exn.result list; |
27814 | 92 |
|
93 |
datatype slot = |
|
94 |
Slot | |
|
95 |
Value of value option | |
|
32738 | 96 |
Assignable of value option Unsynchronized.ref; |
27814 | 97 |
|
98 |
||
5825 | 99 |
(* datatype token *) |
100 |
||
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
101 |
datatype kind = |
27814 | 102 |
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | |
55033 | 103 |
Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue | |
40958
755f8fe7ced9
eliminated obsolete Token.Malformed -- subsumed by Token.Error;
wenzelm
parents:
40627
diff
changeset
|
104 |
Error of string | Sync | EOF; |
5825 | 105 |
|
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
106 |
datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot; |
5825 | 107 |
|
108 |
val str_of_kind = |
|
7026 | 109 |
fn Command => "command" |
110 |
| Keyword => "keyword" |
|
5825 | 111 |
| Ident => "identifier" |
112 |
| LongIdent => "long identifier" |
|
113 |
| SymIdent => "symbolic identifier" |
|
114 |
| Var => "schematic variable" |
|
115 |
| TypeIdent => "type variable" |
|
116 |
| TypeVar => "schematic type variable" |
|
40290
47f572aff50a
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38229
diff
changeset
|
117 |
| Nat => "natural number" |
47f572aff50a
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38229
diff
changeset
|
118 |
| Float => "floating-point number" |
55103 | 119 |
| String => "quoted string" |
17164
a786e1a1ce02
added AltString token (delimited by ASCII back-quotes);
wenzelm
parents:
17069
diff
changeset
|
120 |
| AltString => "back-quoted string" |
5825 | 121 |
| Verbatim => "verbatim text" |
55103 | 122 |
| Cartouche => "text cartouche" |
7682
46de8064c93c
added Space, Comment token kinds (keep actual text);
wenzelm
parents:
7477
diff
changeset
|
123 |
| Space => "white space" |
46de8064c93c
added Space, Comment token kinds (keep actual text);
wenzelm
parents:
7477
diff
changeset
|
124 |
| Comment => "comment text" |
27814 | 125 |
| InternalValue => "internal value" |
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset
|
126 |
| Error _ => "bad input" |
23788
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset
|
127 |
| Sync => "sync marker" |
48911
5debc3e4fa81
tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents:
48905
diff
changeset
|
128 |
| EOF => "end-of-input"; |
5825 | 129 |
|
130 |
||
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
131 |
(* position *) |
5825 | 132 |
|
55708 | 133 |
fun pos_of (Token ((_, (pos, _)), _, _)) = pos; |
134 |
fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos; |
|
27663 | 135 |
|
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
136 |
fun range_of (toks as tok :: _) = |
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
137 |
let val pos' = end_pos_of (List.last toks) |
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
138 |
in Position.range (pos_of tok) pos' end |
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
139 |
| range_of [] = Position.no_range; |
5825 | 140 |
|
141 |
||
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
142 |
(* control tokens *) |
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
143 |
|
27814 | 144 |
fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot); |
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
145 |
val eof = mk_eof Position.none; |
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
146 |
|
27814 | 147 |
fun is_eof (Token (_, (EOF, _), _)) = true |
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
148 |
| is_eof _ = false; |
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
149 |
|
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
150 |
val not_eof = not o is_eof; |
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
151 |
|
27814 | 152 |
fun not_sync (Token (_, (Sync, _), _)) = false |
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
153 |
| not_sync _ = true; |
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
154 |
|
27752
ea7d573e565f
removed obsolete range_of (already included in position);
wenzelm
parents:
27747
diff
changeset
|
155 |
val stopper = |
55708 | 156 |
Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; |
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
157 |
|
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
158 |
|
5825 | 159 |
(* kind of token *) |
160 |
||
27814 | 161 |
fun kind_of (Token (_, (k, _), _)) = k; |
162 |
fun is_kind k (Token (_, (k', _), _)) = k = k'; |
|
5825 | 163 |
|
46811
03a2dc9e0624
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents:
45666
diff
changeset
|
164 |
val is_command = is_kind Command; |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
165 |
val is_name = is_kind Ident orf is_kind SymIdent orf is_kind String orf is_kind Nat; |
46811
03a2dc9e0624
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents:
45666
diff
changeset
|
166 |
|
27814 | 167 |
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x |
7026 | 168 |
| keyword_with _ _ = false; |
5825 | 169 |
|
27814 | 170 |
fun ident_with pred (Token (_, (Ident, x), _)) = pred x |
16029 | 171 |
| ident_with _ _ = false; |
172 |
||
27814 | 173 |
fun is_proper (Token (_, (Space, _), _)) = false |
174 |
| is_proper (Token (_, (Comment, _), _)) = false |
|
5825 | 175 |
| is_proper _ = true; |
176 |
||
51266
3007d0bc9cb1
unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents:
50239
diff
changeset
|
177 |
val is_improper = not o is_proper; |
3007d0bc9cb1
unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents:
50239
diff
changeset
|
178 |
|
27814 | 179 |
fun is_semicolon (Token (_, (Keyword, ";"), _)) = true |
9130 | 180 |
| is_semicolon _ = false; |
181 |
||
27814 | 182 |
fun is_comment (Token (_, (Comment, _), _)) = true |
17069 | 183 |
| is_comment _ = false; |
184 |
||
27814 | 185 |
fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true |
8580 | 186 |
| is_begin_ignore _ = false; |
187 |
||
27814 | 188 |
fun is_end_ignore (Token (_, (Comment, ">"), _)) = true |
8580 | 189 |
| is_end_ignore _ = false; |
190 |
||
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48743
diff
changeset
|
191 |
fun is_error (Token (_, (Error _, _), _)) = true |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48743
diff
changeset
|
192 |
| is_error _ = false; |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48743
diff
changeset
|
193 |
|
8651 | 194 |
|
17069 | 195 |
(* blanks and newlines -- space tokens obey lines *) |
8651 | 196 |
|
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset
|
197 |
fun is_space (Token (_, (Space, _), _)) = true |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset
|
198 |
| is_space _ = false; |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset
|
199 |
|
27814 | 200 |
fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x) |
17069 | 201 |
| is_blank _ = false; |
202 |
||
27814 | 203 |
fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x |
8651 | 204 |
| is_newline _ = false; |
205 |
||
5825 | 206 |
|
14991 | 207 |
(* token content *) |
9155 | 208 |
|
55111 | 209 |
fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) = |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
210 |
if YXML.detect x then x |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49866
diff
changeset
|
211 |
else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source])); |
25642
ebdff0dca2a5
text_of: made even more robust against recurrent errors;
wenzelm
parents:
25582
diff
changeset
|
212 |
|
27885 | 213 |
fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos); |
27873 | 214 |
|
27814 | 215 |
fun content_of (Token (_, (_, x), _)) = x; |
27747
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset
|
216 |
|
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset
|
217 |
|
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
218 |
(* markup *) |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
219 |
|
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
220 |
local |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
221 |
|
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
222 |
val token_kind_markup = |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
223 |
fn Command => (Markup.keyword1, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
224 |
| Keyword => (Markup.keyword2, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
225 |
| Ident => (Markup.empty, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
226 |
| LongIdent => (Markup.empty, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
227 |
| SymIdent => (Markup.empty, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
228 |
| Var => (Markup.var, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
229 |
| TypeIdent => (Markup.tfree, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
230 |
| TypeVar => (Markup.tvar, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
231 |
| Nat => (Markup.empty, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
232 |
| Float => (Markup.empty, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
233 |
| String => (Markup.string, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
234 |
| AltString => (Markup.altstring, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
235 |
| Verbatim => (Markup.verbatim, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
236 |
| Cartouche => (Markup.cartouche, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
237 |
| Space => (Markup.empty, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
238 |
| Comment => (Markup.comment, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
239 |
| InternalValue => (Markup.empty, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
240 |
| Error msg => (Markup.bad, msg) |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
241 |
| Sync => (Markup.control, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
242 |
| EOF => (Markup.control, ""); |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
243 |
|
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
244 |
in |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
245 |
|
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
246 |
fun markup tok = |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
247 |
if keyword_with (not o Symbol.is_ascii_identifier) tok |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
248 |
then (Markup.operator, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
249 |
else token_kind_markup (kind_of tok); |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
250 |
|
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
251 |
end; |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
252 |
|
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
253 |
|
27747
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset
|
254 |
(* unparse *) |
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset
|
255 |
|
27814 | 256 |
fun unparse (Token (_, (kind, x), _)) = |
14991 | 257 |
(case kind of |
43773 | 258 |
String => Symbol_Pos.quote_string_qq x |
259 |
| AltString => Symbol_Pos.quote_string_bq x |
|
260 |
| Verbatim => enclose "{*" "*}" x |
|
55033 | 261 |
| Cartouche => cartouche x |
43773 | 262 |
| Comment => enclose "(*" "*)" x |
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset
|
263 |
| Sync => "" |
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset
|
264 |
| EOF => "" |
14991 | 265 |
| _ => x); |
266 |
||
55745 | 267 |
fun print tok = Markup.markup (#1 (markup tok)) (unparse tok); |
268 |
||
23788
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset
|
269 |
fun text_of tok = |
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset
|
270 |
if is_semicolon tok then ("terminator", "") |
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset
|
271 |
else |
23788
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset
|
272 |
let |
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset
|
273 |
val k = str_of_kind (kind_of tok); |
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
274 |
val (m, _) = markup tok; |
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40290
diff
changeset
|
275 |
val s = unparse tok; |
23788
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset
|
276 |
in |
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset
|
277 |
if s = "" then (k, "") |
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
278 |
else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
279 |
then (k ^ " " ^ Markup.markup m s, "") |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
280 |
else (k, Markup.markup m s) |
23788
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset
|
281 |
end; |
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset
|
282 |
|
5825 | 283 |
|
284 |
||
27814 | 285 |
(** associated values **) |
286 |
||
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
287 |
(* inlined file content *) |
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
288 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
51266
diff
changeset
|
289 |
fun get_files (Token (_, _, Value (SOME (Files files)))) = files |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
51266
diff
changeset
|
290 |
| get_files _ = []; |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
291 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
51266
diff
changeset
|
292 |
fun put_files [] tok = tok |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
51266
diff
changeset
|
293 |
| put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files))) |
55708 | 294 |
| put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok)); |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
295 |
|
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
296 |
|
27814 | 297 |
(* access values *) |
298 |
||
299 |
fun get_value (Token (_, _, Value v)) = v |
|
300 |
| get_value _ = NONE; |
|
301 |
||
302 |
fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v))) |
|
303 |
| map_value _ tok = tok; |
|
304 |
||
305 |
||
306 |
(* make values *) |
|
307 |
||
308 |
fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v)); |
|
309 |
||
310 |
val mk_text = mk_value "<text>" o Text; |
|
311 |
val mk_typ = mk_value "<typ>" o Typ; |
|
312 |
val mk_term = mk_value "<term>" o Term; |
|
313 |
val mk_fact = mk_value "<fact>" o Fact; |
|
314 |
val mk_attribute = mk_value "<attribute>" o Attribute; |
|
315 |
||
316 |
||
317 |
(* static binding *) |
|
318 |
||
319 |
(*1st stage: make empty slots assignable*) |
|
32738 | 320 |
fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE)) |
27814 | 321 |
| assignable tok = tok; |
322 |
||
323 |
(*2nd stage: assign values as side-effect of scanning*) |
|
324 |
fun assign v (Token (_, _, Assignable r)) = r := v |
|
325 |
| assign _ _ = (); |
|
326 |
||
327 |
(*3rd stage: static closure of final values*) |
|
32738 | 328 |
fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v) |
27814 | 329 |
| closure tok = tok; |
330 |
||
331 |
||
332 |
||
5825 | 333 |
(** scanners **) |
334 |
||
30573 | 335 |
open Basic_Symbol_Pos; |
5825 | 336 |
|
48764 | 337 |
val err_prefix = "Outer lexical error: "; |
338 |
||
339 |
fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); |
|
5825 | 340 |
|
341 |
||
342 |
(* scan symbolic idents *) |
|
343 |
||
8231 | 344 |
val scan_symid = |
55033 | 345 |
Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) || |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
346 |
Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single; |
5825 | 347 |
|
8231 | 348 |
fun is_symid str = |
349 |
(case try Symbol.explode str of |
|
55033 | 350 |
SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s |
351 |
| SOME ss => forall Symbol.is_symbolic_char ss |
|
8231 | 352 |
| _ => false); |
353 |
||
27814 | 354 |
fun ident_or_symbolic "begin" = false |
355 |
| ident_or_symbolic ":" = true |
|
356 |
| ident_or_symbolic "::" = true |
|
50239 | 357 |
| ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; |
5825 | 358 |
|
359 |
||
360 |
(* scan verbatim text *) |
|
361 |
||
362 |
val scan_verb = |
|
55107 | 363 |
$$$ "*" --| Scan.ahead (~$$ "}") || |
27769 | 364 |
Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single; |
5825 | 365 |
|
366 |
val scan_verbatim = |
|
55107 | 367 |
Scan.ahead ($$ "{" -- $$ "*") |-- |
55106 | 368 |
!!! "unclosed verbatim text" |
55107 | 369 |
((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- |
55106 | 370 |
Symbol_Pos.change_prompt |
55107 | 371 |
((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); |
5825 | 372 |
|
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset
|
373 |
val recover_verbatim = |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset
|
374 |
$$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat); |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset
|
375 |
|
5825 | 376 |
|
55033 | 377 |
(* scan cartouche *) |
378 |
||
379 |
val scan_cartouche = |
|
55104
8284c0d5bf52
clarified scan_cartouche_depth, according to Scala version;
wenzelm
parents:
55103
diff
changeset
|
380 |
Symbol_Pos.scan_pos -- |
55105 | 381 |
((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos); |
55033 | 382 |
|
383 |
||
5825 | 384 |
(* scan space *) |
385 |
||
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset
|
386 |
fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n"; |
5825 | 387 |
|
388 |
val scan_space = |
|
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset
|
389 |
Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] || |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset
|
390 |
Scan.many space_symbol @@@ $$$ "\n"; |
5825 | 391 |
|
392 |
||
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
393 |
(* scan comment *) |
5825 | 394 |
|
395 |
val scan_comment = |
|
55105 | 396 |
Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos); |
5825 | 397 |
|
398 |
||
27663 | 399 |
|
27769 | 400 |
(** token sources **) |
5825 | 401 |
|
27769 | 402 |
fun source_proper src = src |> Source.filter is_proper; |
5825 | 403 |
|
23678 | 404 |
local |
405 |
||
27769 | 406 |
fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
407 |
|
27799 | 408 |
fun token k ss = |
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
42503
diff
changeset
|
409 |
Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); |
27799 | 410 |
|
411 |
fun token_range k (pos1, (ss, pos2)) = |
|
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
42503
diff
changeset
|
412 |
Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot); |
23678 | 413 |
|
27769 | 414 |
fun scan (lex1, lex2) = !!! "bad input" |
48764 | 415 |
(Symbol_Pos.scan_string_qq err_prefix >> token_range String || |
416 |
Symbol_Pos.scan_string_bq err_prefix >> token_range AltString || |
|
27799 | 417 |
scan_verbatim >> token_range Verbatim || |
55033 | 418 |
scan_cartouche >> token_range Cartouche || |
27799 | 419 |
scan_comment >> token_range Comment || |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
420 |
scan_space >> token Space || |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
421 |
Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) || |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
422 |
(Scan.max token_leq |
27769 | 423 |
(Scan.max token_leq |
424 |
(Scan.literal lex2 >> pair Command) |
|
425 |
(Scan.literal lex1 >> pair Keyword)) |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
426 |
(Lexicon.scan_longid >> pair LongIdent || |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
427 |
Lexicon.scan_id >> pair Ident || |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
428 |
Lexicon.scan_var >> pair Var || |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
429 |
Lexicon.scan_tid >> pair TypeIdent || |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
430 |
Lexicon.scan_tvar >> pair TypeVar || |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
431 |
Lexicon.scan_float >> pair Float || |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
432 |
Lexicon.scan_nat >> pair Nat || |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
433 |
scan_symid >> pair SymIdent) >> uncurry token)); |
27769 | 434 |
|
435 |
fun recover msg = |
|
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset
|
436 |
(Symbol_Pos.recover_string_qq || |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset
|
437 |
Symbol_Pos.recover_string_bq || |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset
|
438 |
recover_verbatim || |
55033 | 439 |
Symbol_Pos.recover_cartouche || |
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset
|
440 |
Symbol_Pos.recover_comment || |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset
|
441 |
Scan.one (Symbol.is_regular o Symbol_Pos.symbol) >> single) |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
442 |
>> (single o token (Error msg)); |
23678 | 443 |
|
444 |
in |
|
5825 | 445 |
|
27835
ff8b8513965a
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27814
diff
changeset
|
446 |
fun source' {do_recover} get_lex = |
30573 | 447 |
Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs)) |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
448 |
(Option.map (rpair recover) do_recover); |
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
449 |
|
5825 | 450 |
fun source do_recover get_lex pos src = |
30573 | 451 |
Symbol_Pos.source pos src |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
452 |
|> source' do_recover get_lex; |
23678 | 453 |
|
454 |
end; |
|
5825 | 455 |
|
30586
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
456 |
|
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
457 |
(* read_antiq *) |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
458 |
|
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
459 |
fun read_antiq lex scan (syms, pos) = |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
460 |
let |
48992 | 461 |
fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^ |
30586
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
462 |
"@{" ^ Symbol_Pos.content syms ^ "}"); |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
463 |
|
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
464 |
val res = |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
465 |
Source.of_list syms |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
466 |
|> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon)) |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
467 |
|> source_proper |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
468 |
|> Source.source stopper (Scan.error (Scan.bulk scan)) NONE |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
469 |
|> Source.exhaust; |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
470 |
in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end; |
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
471 |
|
5825 | 472 |
end; |