author | wenzelm |
Wed, 03 Dec 2014 11:37:51 +0100 | |
changeset 59081 | 2ceb05ee0331 |
parent 59064 | a8bcb5a446c8 |
child 59083 | 88b0b1f28adc |
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 = |
59081 | 10 |
(*immediate source*) |
11 |
Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | |
|
12 |
Float | Space | |
|
13 |
(*delimited content*) |
|
14 |
String | Alt_String | Verbatim | Cartouche | Comment | |
|
15 |
(*special content*) |
|
16 |
Error of string | Internal_Value | EOF |
|
58012 | 17 |
val str_of_kind: kind -> string |
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55750
diff
changeset
|
18 |
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} |
58012 | 19 |
type T |
20 |
type src |
|
27814 | 21 |
datatype value = |
58012 | 22 |
Source of src | |
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
23 |
Literal of bool * Markup.T | |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
24 |
Name of string * morphism | |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
25 |
Typ of typ | |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
26 |
Term of term | |
57942
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
56202
diff
changeset
|
27 |
Fact of string option * thm list | |
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
28 |
Attribute of morphism -> attribute | |
58017 | 29 |
Declaration of declaration | |
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
30 |
Files of file Exn.result list |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
31 |
val name0: string -> value |
55708 | 32 |
val pos_of: T -> Position.T |
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
33 |
val range_of: T list -> Position.range |
58012 | 34 |
val src: xstring * Position.T -> T list -> src |
35 |
val name_of_src: src -> string * Position.T |
|
36 |
val args_of_src: src -> T list |
|
37 |
val range_of_src: src -> Position.T |
|
38 |
val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a |
|
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
39 |
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
|
40 |
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
|
41 |
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
|
42 |
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
|
43 |
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
|
44 |
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
|
45 |
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
|
46 |
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
|
47 |
val is_command: T -> bool |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
48 |
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
|
49 |
val is_proper: T -> bool |
51266
3007d0bc9cb1
unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents:
50239
diff
changeset
|
50 |
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
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
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
|
56 |
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
|
57 |
val is_newline: T -> bool |
55111 | 58 |
val inner_syntax_of: T -> string |
59064 | 59 |
val source_position_of: T -> Input.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
|
60 |
val content_of: T -> string |
56202 | 61 |
val keyword_markup: bool * Markup.T -> string -> Markup.T |
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
62 |
val completion_report: T -> Position.report_text list |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
63 |
val report: T -> Position.report_text |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
64 |
val markup: T -> Markup.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
|
65 |
val unparse: T -> string |
58012 | 66 |
val unparse_src: src -> string list |
55745 | 67 |
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
|
68 |
val text_of: T -> string * string |
54520
cee77d2e9582
release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents:
54519
diff
changeset
|
69 |
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
|
70 |
val put_files: file Exn.result list -> T -> T |
58025 | 71 |
val make_value: string -> value -> 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
|
72 |
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
|
73 |
val map_value: (value -> value) -> T -> T |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55828
diff
changeset
|
74 |
val reports_of_value: T -> Position.report list |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
75 |
val transform: morphism -> T -> T |
58012 | 76 |
val transform_src: morphism -> src -> src |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55828
diff
changeset
|
77 |
val init_assignable: T -> T |
58012 | 78 |
val init_assignable_src: src -> src |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
79 |
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
|
80 |
val closure: T -> T |
58012 | 81 |
val closure_src: src -> src |
82 |
val pretty_value: Proof.context -> T -> Pretty.T |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
83 |
val pretty_src: Proof.context -> src -> Pretty.T |
27814 | 84 |
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
|
85 |
val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source |
58904
f49c4f883c58
eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents:
58903
diff
changeset
|
86 |
val source: Keyword.keywords -> |
58864 | 87 |
Position.T -> (Symbol.symbol, 'a) Source.source -> (T, |
88 |
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source |
|
58904
f49c4f883c58
eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents:
58903
diff
changeset
|
89 |
val source_strict: Keyword.keywords -> |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
90 |
Position.T -> (Symbol.symbol, 'a) Source.source -> (T, |
30573 | 91 |
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
92 |
type 'a parser = T list -> 'a * T list |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
93 |
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list) |
58903 | 94 |
val read_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list |
95 |
val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
96 |
val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
97 |
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context |
5825 | 98 |
end; |
99 |
||
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
100 |
structure Token: TOKEN = |
5825 | 101 |
struct |
102 |
||
103 |
(** tokens **) |
|
104 |
||
58012 | 105 |
(* token kind *) |
5825 | 106 |
|
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset
|
107 |
datatype kind = |
59081 | 108 |
(*immediate source*) |
109 |
Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | |
|
110 |
Float | Space | |
|
111 |
(*delimited content*) |
|
112 |
String | Alt_String | Verbatim | Cartouche | Comment | |
|
113 |
(*special content*) |
|
114 |
Error of string | Internal_Value | EOF; |
|
5825 | 115 |
|
116 |
val str_of_kind = |
|
7026 | 117 |
fn Command => "command" |
118 |
| Keyword => "keyword" |
|
5825 | 119 |
| Ident => "identifier" |
59081 | 120 |
| Long_Ident => "long identifier" |
121 |
| Sym_Ident => "symbolic identifier" |
|
5825 | 122 |
| Var => "schematic variable" |
59081 | 123 |
| Type_Ident => "type variable" |
124 |
| Type_Var => "schematic type variable" |
|
40290
47f572aff50a
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38229
diff
changeset
|
125 |
| Nat => "natural number" |
47f572aff50a
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38229
diff
changeset
|
126 |
| Float => "floating-point number" |
59081 | 127 |
| Space => "white space" |
55103 | 128 |
| String => "quoted string" |
59081 | 129 |
| Alt_String => "back-quoted string" |
5825 | 130 |
| Verbatim => "verbatim text" |
55103 | 131 |
| Cartouche => "text cartouche" |
7682
46de8064c93c
added Space, Comment token kinds (keep actual text);
wenzelm
parents:
7477
diff
changeset
|
132 |
| Comment => "comment text" |
59081 | 133 |
| Internal_Value => "internal value" |
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset
|
134 |
| Error _ => "bad input" |
48911
5debc3e4fa81
tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents:
48905
diff
changeset
|
135 |
| EOF => "end-of-input"; |
5825 | 136 |
|
59081 | 137 |
val delimited_kind = member (op =) [String, Alt_String, Verbatim, Cartouche, Comment]; |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset
|
138 |
|
5825 | 139 |
|
58012 | 140 |
(* datatype token *) |
141 |
||
142 |
(*The value slot assigns an (optional) internal value to a token, |
|
143 |
usually as a side-effect of special scanner setup (see also |
|
144 |
args.ML). Note that an assignable ref designates an intermediate |
|
145 |
state of internalization -- it is NOT meant to persist.*) |
|
146 |
||
147 |
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}; |
|
148 |
||
149 |
datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot |
|
150 |
||
151 |
and src = |
|
152 |
Src of |
|
153 |
{name: string * Position.T, |
|
154 |
args: T list, |
|
155 |
output_info: (string * Markup.T) option} |
|
156 |
||
157 |
and slot = |
|
158 |
Slot | |
|
159 |
Value of value option | |
|
160 |
Assignable of value option Unsynchronized.ref |
|
161 |
||
162 |
and value = |
|
163 |
Source of src | |
|
164 |
Literal of bool * Markup.T | |
|
165 |
Name of string * morphism | |
|
166 |
Typ of typ | |
|
167 |
Term of term | |
|
168 |
Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) |
|
169 |
Attribute of morphism -> attribute | |
|
58017 | 170 |
Declaration of declaration | |
58012 | 171 |
Files of file Exn.result list; |
172 |
||
173 |
fun name0 a = Name (a, Morphism.identity); |
|
174 |
||
175 |
||
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
176 |
(* position *) |
5825 | 177 |
|
55708 | 178 |
fun pos_of (Token ((_, (pos, _)), _, _)) = pos; |
179 |
fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos; |
|
27663 | 180 |
|
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
181 |
fun range_of (toks as tok :: _) = |
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
182 |
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
|
183 |
in Position.range (pos_of tok) pos' end |
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
184 |
| range_of [] = Position.no_range; |
5825 | 185 |
|
186 |
||
58012 | 187 |
(* src *) |
188 |
||
189 |
fun src name args = Src {name = name, args = args, output_info = NONE}; |
|
190 |
||
191 |
fun map_args f (Src {name, args, output_info}) = |
|
192 |
Src {name = name, args = map f args, output_info = output_info}; |
|
193 |
||
194 |
fun name_of_src (Src {name, ...}) = name; |
|
195 |
fun args_of_src (Src {args, ...}) = args; |
|
196 |
||
197 |
fun range_of_src (Src {name = (_, pos), args, ...}) = |
|
198 |
if null args then pos |
|
199 |
else Position.set_range (pos, #2 (range_of args)); |
|
200 |
||
201 |
fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) = |
|
202 |
let |
|
203 |
val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos); |
|
204 |
val space = Name_Space.space_of_table table; |
|
205 |
val kind = Name_Space.kind_of space; |
|
206 |
val markup = Name_Space.markup space name; |
|
207 |
in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end; |
|
208 |
||
209 |
||
58855 | 210 |
(* stopper *) |
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
211 |
|
27814 | 212 |
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
|
213 |
val eof = mk_eof Position.none; |
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
214 |
|
27814 | 215 |
fun is_eof (Token (_, (EOF, _), _)) = true |
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
216 |
| is_eof _ = false; |
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
217 |
|
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
218 |
val not_eof = not o is_eof; |
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
219 |
|
27752
ea7d573e565f
removed obsolete range_of (already included in position);
wenzelm
parents:
27747
diff
changeset
|
220 |
val stopper = |
55708 | 221 |
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
|
222 |
|
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset
|
223 |
|
5825 | 224 |
(* kind of token *) |
225 |
||
27814 | 226 |
fun kind_of (Token (_, (k, _), _)) = k; |
227 |
fun is_kind k (Token (_, (k', _), _)) = k = k'; |
|
5825 | 228 |
|
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
|
229 |
val is_command = is_kind Command; |
59081 | 230 |
val is_name = is_kind Ident orf is_kind Sym_Ident 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
|
231 |
|
27814 | 232 |
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x |
7026 | 233 |
| keyword_with _ _ = false; |
5825 | 234 |
|
27814 | 235 |
fun ident_with pred (Token (_, (Ident, x), _)) = pred x |
16029 | 236 |
| ident_with _ _ = false; |
237 |
||
27814 | 238 |
fun is_proper (Token (_, (Space, _), _)) = false |
239 |
| is_proper (Token (_, (Comment, _), _)) = false |
|
5825 | 240 |
| is_proper _ = true; |
241 |
||
51266
3007d0bc9cb1
unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents:
50239
diff
changeset
|
242 |
val is_improper = not o is_proper; |
3007d0bc9cb1
unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents:
50239
diff
changeset
|
243 |
|
27814 | 244 |
fun is_comment (Token (_, (Comment, _), _)) = true |
17069 | 245 |
| is_comment _ = false; |
246 |
||
27814 | 247 |
fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true |
8580 | 248 |
| is_begin_ignore _ = false; |
249 |
||
27814 | 250 |
fun is_end_ignore (Token (_, (Comment, ">"), _)) = true |
8580 | 251 |
| is_end_ignore _ = false; |
252 |
||
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48743
diff
changeset
|
253 |
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
|
254 |
| 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
|
255 |
|
8651 | 256 |
|
17069 | 257 |
(* blanks and newlines -- space tokens obey lines *) |
8651 | 258 |
|
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
|
259 |
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
|
260 |
| 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
|
261 |
|
27814 | 262 |
fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x) |
17069 | 263 |
| is_blank _ = false; |
264 |
||
27814 | 265 |
fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x |
8651 | 266 |
| is_newline _ = false; |
267 |
||
5825 | 268 |
|
14991 | 269 |
(* token content *) |
9155 | 270 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset
|
271 |
fun inner_syntax_of (Token ((source, (pos, _)), (kind, 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
|
272 |
if YXML.detect x then x |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset
|
273 |
else |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset
|
274 |
let |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset
|
275 |
val delimited = delimited_kind kind; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset
|
276 |
val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]); |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset
|
277 |
in YXML.string_of tree end; |
25642
ebdff0dca2a5
text_of: made even more robust against recurrent errors;
wenzelm
parents:
25582
diff
changeset
|
278 |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58904
diff
changeset
|
279 |
fun source_position_of (Token ((source, range), (kind, _), _)) = |
59064 | 280 |
Input.source (delimited_kind kind) source range; |
27873 | 281 |
|
27814 | 282 |
fun content_of (Token (_, (_, x), _)) = x; |
27747
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset
|
283 |
|
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset
|
284 |
|
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
285 |
(* markup reports *) |
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
286 |
|
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
287 |
local |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
288 |
|
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
289 |
val token_kind_markup = |
59081 | 290 |
fn Command => (Markup.command, "") |
291 |
| Keyword => (Markup.keyword2, "") |
|
292 |
| Ident => (Markup.empty, "") |
|
293 |
| Long_Ident => (Markup.empty, "") |
|
294 |
| Sym_Ident => (Markup.empty, "") |
|
295 |
| Var => (Markup.var, "") |
|
296 |
| Type_Ident => (Markup.tfree, "") |
|
297 |
| Type_Var => (Markup.tvar, "") |
|
298 |
| Nat => (Markup.empty, "") |
|
299 |
| Float => (Markup.empty, "") |
|
300 |
| Space => (Markup.empty, "") |
|
301 |
| String => (Markup.string, "") |
|
302 |
| Alt_String => (Markup.alt_string, "") |
|
303 |
| Verbatim => (Markup.verbatim, "") |
|
304 |
| Cartouche => (Markup.cartouche, "") |
|
305 |
| Comment => (Markup.comment, "") |
|
306 |
| Error msg => (Markup.bad, msg) |
|
307 |
| Internal_Value => (Markup.empty, "") |
|
308 |
| EOF => (Markup.empty, ""); |
|
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
309 |
|
56063 | 310 |
in |
311 |
||
56202 | 312 |
fun keyword_markup (important, keyword) x = |
313 |
if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter; |
|
55919
2eb8c13339a5
more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
wenzelm
parents:
55916
diff
changeset
|
314 |
|
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
315 |
fun completion_report tok = |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55828
diff
changeset
|
316 |
if is_kind Keyword tok |
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
317 |
then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
318 |
else []; |
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
319 |
|
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
320 |
fun report tok = |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
321 |
if is_kind Keyword tok then |
56202 | 322 |
((pos_of tok, keyword_markup (false, Markup.keyword2) (content_of tok)), "") |
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
323 |
else |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
324 |
let val (m, text) = token_kind_markup (kind_of tok) |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
325 |
in ((pos_of tok, m), text) end; |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
326 |
|
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
327 |
val markup = #2 o #1 o report; |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55828
diff
changeset
|
328 |
|
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
329 |
end; |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
330 |
|
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset
|
331 |
|
27747
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset
|
332 |
(* unparse *) |
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset
|
333 |
|
27814 | 334 |
fun unparse (Token (_, (kind, x), _)) = |
14991 | 335 |
(case kind of |
43773 | 336 |
String => Symbol_Pos.quote_string_qq x |
59081 | 337 |
| Alt_String => Symbol_Pos.quote_string_bq x |
43773 | 338 |
| Verbatim => enclose "{*" "*}" x |
55033 | 339 |
| Cartouche => cartouche x |
43773 | 340 |
| Comment => enclose "(*" "*)" x |
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset
|
341 |
| EOF => "" |
14991 | 342 |
| _ => x); |
343 |
||
58012 | 344 |
fun unparse_src (Src {args, ...}) = map unparse args; |
345 |
||
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55914
diff
changeset
|
346 |
fun print tok = Markup.markup (markup tok) (unparse tok); |
55745 | 347 |
|
23788
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset
|
348 |
fun text_of tok = |
58861
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
349 |
let |
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
350 |
val k = str_of_kind (kind_of tok); |
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
351 |
val m = markup tok; |
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
352 |
val s = unparse tok; |
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
353 |
in |
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
354 |
if s = "" then (k, "") |
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
355 |
else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) |
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
356 |
then (k ^ " " ^ Markup.markup m s, "") |
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
357 |
else (k, Markup.markup m s) |
5ff61774df11
command-line terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset
|
358 |
end; |
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset
|
359 |
|
5825 | 360 |
|
361 |
||
27814 | 362 |
(** associated values **) |
363 |
||
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
364 |
(* inlined file content *) |
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
365 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
51266
diff
changeset
|
366 |
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
|
367 |
| get_files _ = []; |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
368 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
51266
diff
changeset
|
369 |
fun put_files [] tok = tok |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
51266
diff
changeset
|
370 |
| put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files))) |
55708 | 371 |
| 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
|
372 |
|
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset
|
373 |
|
27814 | 374 |
(* access values *) |
375 |
||
58025 | 376 |
fun make_value name v = |
59081 | 377 |
Token ((name, Position.no_range), (Internal_Value, name), Value (SOME v)); |
58025 | 378 |
|
27814 | 379 |
fun get_value (Token (_, _, Value v)) = v |
380 |
| get_value _ = NONE; |
|
381 |
||
382 |
fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v))) |
|
383 |
| map_value _ tok = tok; |
|
384 |
||
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55828
diff
changeset
|
385 |
fun reports_of_value tok = |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55828
diff
changeset
|
386 |
(case get_value tok of |
56063 | 387 |
SOME (Literal markup) => |
388 |
let |
|
389 |
val pos = pos_of tok; |
|
390 |
val x = content_of tok; |
|
391 |
in |
|
392 |
if Position.is_reported pos then |
|
393 |
map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x) |
|
394 |
else [] |
|
395 |
end |
|
396 |
| _ => []); |
|
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55828
diff
changeset
|
397 |
|
27814 | 398 |
|
58012 | 399 |
(* transform *) |
400 |
||
401 |
fun transform phi = |
|
402 |
map_value (fn v => |
|
403 |
(case v of |
|
404 |
Source src => Source (transform_src phi src) |
|
405 |
| Literal _ => v |
|
406 |
| Name (a, psi) => Name (a, psi $> phi) |
|
407 |
| Typ T => Typ (Morphism.typ phi T) |
|
408 |
| Term t => Term (Morphism.term phi t) |
|
409 |
| Fact (a, ths) => Fact (a, Morphism.fact phi ths) |
|
410 |
| Attribute att => Attribute (Morphism.transform phi att) |
|
58017 | 411 |
| Declaration decl => Declaration (Morphism.transform phi decl) |
58012 | 412 |
| Files _ => v)) |
413 |
and transform_src phi = map_args (transform phi); |
|
414 |
||
415 |
||
416 |
(* static binding *) |
|
417 |
||
418 |
(*1st stage: initialize assignable slots*) |
|
419 |
fun init_assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE)) |
|
420 |
| init_assignable (tok as Token (_, _, Assignable r)) = (r := NONE; tok) |
|
421 |
| init_assignable tok = tok; |
|
422 |
||
423 |
val init_assignable_src = map_args init_assignable; |
|
424 |
||
425 |
(*2nd stage: assign values as side-effect of scanning*) |
|
426 |
fun assign v (Token (_, _, Assignable r)) = r := v |
|
427 |
| assign _ _ = (); |
|
428 |
||
429 |
(*3rd stage: static closure of final values*) |
|
430 |
fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v) |
|
431 |
| closure tok = tok; |
|
432 |
||
433 |
val closure_src = map_args closure; |
|
434 |
||
435 |
||
436 |
(* pretty *) |
|
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
437 |
|
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
438 |
fun pretty_value ctxt tok = |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
439 |
(case get_value tok of |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
440 |
SOME (Literal markup) => |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
441 |
let val x = content_of tok |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
442 |
in Pretty.mark_str (keyword_markup markup x, x) end |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
443 |
| SOME (Name (a, _)) => Pretty.str (quote a) |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
444 |
| SOME (Typ T) => Syntax.pretty_typ ctxt T |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
445 |
| SOME (Term t) => Syntax.pretty_term ctxt t |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
446 |
| SOME (Fact (_, ths)) => |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
447 |
Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths)) |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
448 |
| _ => Pretty.mark_str (markup tok, unparse tok)); |
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset
|
449 |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
450 |
fun pretty_src ctxt src = |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
451 |
let |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
452 |
val Src {name = (name, _), args, output_info} = src; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
453 |
val prt_name = |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
454 |
(case output_info of |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
455 |
NONE => Pretty.str name |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
456 |
| SOME (_, markup) => Pretty.mark_str (markup, name)); |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
457 |
val prt_arg = pretty_value ctxt; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
458 |
in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
459 |
|
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
460 |
|
5825 | 461 |
(** scanners **) |
462 |
||
30573 | 463 |
open Basic_Symbol_Pos; |
5825 | 464 |
|
48764 | 465 |
val err_prefix = "Outer lexical error: "; |
466 |
||
467 |
fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); |
|
5825 | 468 |
|
469 |
||
470 |
(* scan symbolic idents *) |
|
471 |
||
8231 | 472 |
val scan_symid = |
55033 | 473 |
Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) || |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
474 |
Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single; |
5825 | 475 |
|
8231 | 476 |
fun is_symid str = |
477 |
(case try Symbol.explode str of |
|
55033 | 478 |
SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s |
479 |
| SOME ss => forall Symbol.is_symbolic_char ss |
|
8231 | 480 |
| _ => false); |
481 |
||
27814 | 482 |
fun ident_or_symbolic "begin" = false |
483 |
| ident_or_symbolic ":" = true |
|
484 |
| ident_or_symbolic "::" = true |
|
50239 | 485 |
| ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; |
5825 | 486 |
|
487 |
||
488 |
(* scan verbatim text *) |
|
489 |
||
490 |
val scan_verb = |
|
55107 | 491 |
$$$ "*" --| Scan.ahead (~$$ "}") || |
58854 | 492 |
Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single; |
5825 | 493 |
|
494 |
val scan_verbatim = |
|
55107 | 495 |
Scan.ahead ($$ "{" -- $$ "*") |-- |
55106 | 496 |
!!! "unclosed verbatim text" |
55107 | 497 |
((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- |
58850 | 498 |
((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); |
5825 | 499 |
|
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset
|
500 |
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
|
501 |
$$$ "{" @@@ $$$ "*" @@@ (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
|
502 |
|
5825 | 503 |
|
55033 | 504 |
(* scan cartouche *) |
505 |
||
506 |
val scan_cartouche = |
|
55104
8284c0d5bf52
clarified scan_cartouche_depth, according to Scala version;
wenzelm
parents:
55103
diff
changeset
|
507 |
Symbol_Pos.scan_pos -- |
55105 | 508 |
((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos); |
55033 | 509 |
|
510 |
||
5825 | 511 |
(* scan space *) |
512 |
||
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
|
513 |
fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n"; |
5825 | 514 |
|
515 |
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
|
516 |
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
|
517 |
Scan.many space_symbol @@@ $$$ "\n"; |
5825 | 518 |
|
519 |
||
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
520 |
(* scan comment *) |
5825 | 521 |
|
522 |
val scan_comment = |
|
55105 | 523 |
Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos); |
5825 | 524 |
|
525 |
||
27663 | 526 |
|
27769 | 527 |
(** token sources **) |
5825 | 528 |
|
27769 | 529 |
fun source_proper src = src |> Source.filter is_proper; |
5825 | 530 |
|
23678 | 531 |
local |
532 |
||
27769 | 533 |
fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
534 |
|
27799 | 535 |
fun token k ss = |
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
42503
diff
changeset
|
536 |
Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); |
27799 | 537 |
|
538 |
fun token_range k (pos1, (ss, pos2)) = |
|
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
42503
diff
changeset
|
539 |
Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot); |
23678 | 540 |
|
58903 | 541 |
fun scan keywords = !!! "bad input" |
48764 | 542 |
(Symbol_Pos.scan_string_qq err_prefix >> token_range String || |
59081 | 543 |
Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String || |
27799 | 544 |
scan_verbatim >> token_range Verbatim || |
55033 | 545 |
scan_cartouche >> token_range Cartouche || |
27799 | 546 |
scan_comment >> token_range Comment || |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
547 |
scan_space >> token Space || |
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
548 |
(Scan.max token_leq |
27769 | 549 |
(Scan.max token_leq |
58903 | 550 |
(Scan.literal (Keyword.major_keywords keywords) >> pair Command) |
551 |
(Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword)) |
|
59081 | 552 |
(Lexicon.scan_longid >> pair Long_Ident || |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
553 |
Lexicon.scan_id >> pair Ident || |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
554 |
Lexicon.scan_var >> pair Var || |
59081 | 555 |
Lexicon.scan_tid >> pair Type_Ident || |
556 |
Lexicon.scan_tvar >> pair Type_Var || |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
557 |
Lexicon.scan_float >> pair Float || |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset
|
558 |
Lexicon.scan_nat >> pair Nat || |
59081 | 559 |
scan_symid >> pair Sym_Ident) >> uncurry token)); |
27769 | 560 |
|
561 |
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
|
562 |
(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
|
563 |
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
|
564 |
recover_verbatim || |
55033 | 565 |
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
|
566 |
Symbol_Pos.recover_comment || |
58854 | 567 |
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) |
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
568 |
>> (single o token (Error msg)); |
23678 | 569 |
|
570 |
in |
|
5825 | 571 |
|
58904
f49c4f883c58
eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents:
58903
diff
changeset
|
572 |
fun source' strict keywords = |
58864 | 573 |
let |
58904
f49c4f883c58
eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents:
58903
diff
changeset
|
574 |
val scan_strict = Scan.bulk (scan keywords); |
58864 | 575 |
val scan = if strict then scan_strict else Scan.recover scan_strict recover; |
576 |
in Source.source Symbol_Pos.stopper scan end; |
|
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset
|
577 |
|
58904
f49c4f883c58
eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents:
58903
diff
changeset
|
578 |
fun source keywords pos src = Symbol_Pos.source pos src |> source' false keywords; |
f49c4f883c58
eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents:
58903
diff
changeset
|
579 |
fun source_strict keywords pos src = Symbol_Pos.source pos src |> source' true keywords; |
23678 | 580 |
|
581 |
end; |
|
5825 | 582 |
|
30586
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset
|
583 |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
584 |
|
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
585 |
(** parsers **) |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
586 |
|
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
587 |
type 'a parser = T list -> 'a * T list; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
588 |
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list); |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
589 |
|
58045 | 590 |
|
591 |
(* read source *) |
|
592 |
||
58903 | 593 |
fun read_no_commands keywords scan syms = |
58045 | 594 |
Source.of_list syms |
58904
f49c4f883c58
eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents:
58903
diff
changeset
|
595 |
|> source' true (Keyword.no_command_keywords keywords) |
58045 | 596 |
|> source_proper |
58864 | 597 |
|> Source.source stopper (Scan.error (Scan.bulk scan)) |
58045 | 598 |
|> Source.exhaust; |
599 |
||
58903 | 600 |
fun read_antiq keywords scan (syms, pos) = |
58045 | 601 |
let |
602 |
fun err msg = |
|
603 |
cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^ |
|
604 |
"@{" ^ Symbol_Pos.content syms ^ "}"); |
|
58903 | 605 |
val res = read_no_commands keywords scan syms handle ERROR msg => err msg; |
58045 | 606 |
in (case res of [x] => x | _ => err "") end; |
607 |
||
608 |
||
609 |
(* wrapped syntax *) |
|
610 |
||
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
611 |
fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context = |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
612 |
let |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
613 |
val args1 = map init_assignable args0; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
614 |
fun reported_text () = |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
615 |
if Context_Position.is_visible_generic context then |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
616 |
((pos, Markup.operator) :: maps (reports_of_value o closure) args1) |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
617 |
|> map (fn (p, m) => Position.reported_text p m "") |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
618 |
else []; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
619 |
in |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
620 |
(case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
621 |
(SOME x, (context', [])) => |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
622 |
let val _ = Output.report (reported_text ()) |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
623 |
in (x, context') end |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
624 |
| (_, (_, args2)) => |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
625 |
let |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
626 |
val print_name = |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
627 |
(case output_info of |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
628 |
NONE => quote name |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
629 |
| SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name)); |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
630 |
val print_args = |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
631 |
if null args2 then "" else ":\n " ^ space_implode " " (map print args2); |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
632 |
in |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
633 |
error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^ |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
634 |
Markup.markup_report (implode (reported_text ()))) |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
635 |
end) |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
636 |
end; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
637 |
|
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
638 |
fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
639 |
|
5825 | 640 |
end; |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
641 |
|
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
642 |
type 'a parser = 'a Token.parser; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
643 |
type 'a context_parser = 'a Token.context_parser; |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset
|
644 |