author | wenzelm |
Mon, 26 Nov 2012 13:54:43 +0100 | |
changeset 50213 | 7b73c0509835 |
parent 50201 | c26369c9eda6 |
child 50215 | 97959912840a |
permissions | -rw-r--r-- |
5829 | 1 |
(* Title: Pure/Isar/outer_syntax.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
4 |
The global Isabelle/Isar outer syntax. |
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
5 |
|
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
6 |
Note: the syntax for files is statically determined at the very |
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
7 |
beginning; for interactive processing it may change dynamically. |
5829 | 8 |
*) |
9 |
||
10 |
signature OUTER_SYNTAX = |
|
11 |
sig |
|
43711 | 12 |
type outer_syntax |
43712
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43711
diff
changeset
|
13 |
val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool |
43711 | 14 |
val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax |
46970
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
15 |
val check_syntax: unit -> unit |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48638
diff
changeset
|
16 |
type command_spec = (string * Keyword.T) * Position.T |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
17 |
val command: command_spec -> string -> |
29311 | 18 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
19 |
val markup_command: Thy_Output.markup -> command_spec -> string -> |
29311 | 20 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
21 |
val improper_command: command_spec -> string -> |
43711 | 22 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
23 |
val local_theory': command_spec -> string -> |
29380 | 24 |
(bool -> local_theory -> local_theory) parser -> unit |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
25 |
val local_theory: command_spec -> string -> |
29311 | 26 |
(local_theory -> local_theory) parser -> unit |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
27 |
val local_theory_to_proof': command_spec -> string -> |
29311 | 28 |
(bool -> local_theory -> Proof.state) parser -> unit |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
29 |
val local_theory_to_proof: command_spec -> string -> |
29311 | 30 |
(local_theory -> Proof.state) parser -> unit |
50213 | 31 |
val help_outer_syntax: string list -> unit |
5883 | 32 |
val print_outer_syntax: unit -> unit |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset
|
33 |
val scan: Position.T -> string -> Token.T list |
25580 | 34 |
val parse: Position.T -> string -> Toplevel.transition list |
26600 | 35 |
type isar |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
36 |
val isar: TextIO.instream -> bool -> isar |
48918
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
37 |
val span_cmts: Token.T list -> Token.T list |
46876
8f3bb485f628
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
wenzelm
parents:
44736
diff
changeset
|
38 |
val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool |
44478
4fdb1009a370
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
wenzelm
parents:
44357
diff
changeset
|
39 |
val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element -> |
43712
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43711
diff
changeset
|
40 |
(Toplevel.transition * Toplevel.transition list) list |
5829 | 41 |
end; |
42 |
||
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
43 |
structure Outer_Syntax: OUTER_SYNTAX = |
5829 | 44 |
struct |
45 |
||
46 |
(** outer syntax **) |
|
47 |
||
29311 | 48 |
(* command parsers *) |
5829 | 49 |
|
29311 | 50 |
datatype command = Command of |
24868 | 51 |
{comment: string, |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36959
diff
changeset
|
52 |
markup: Thy_Output.markup option, |
24868 | 53 |
int_only: bool, |
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
54 |
parse: (Toplevel.transition -> Toplevel.transition) parser, |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
55 |
pos: Position.T, |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
56 |
id: serial}; |
5829 | 57 |
|
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
58 |
fun new_command comment markup int_only parse pos = |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
59 |
Command {comment = comment, markup = markup, int_only = int_only, parse = parse, |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
60 |
pos = pos, id = serial ()}; |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
61 |
|
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
62 |
fun command_markup def (name, Command {pos, id, ...}) = |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
63 |
Markup.properties (Position.entity_properties_of def id pos) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49564
diff
changeset
|
64 |
(Markup.entity Markup.commandN name); |
5829 | 65 |
|
50213 | 66 |
fun pretty_command (cmd as (name, Command {comment, ...})) = |
67 |
Pretty.block |
|
68 |
(Pretty.marks_str |
|
69 |
([Sendback.make_markup {implicit = true}, command_markup false cmd], name) :: |
|
70 |
Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); |
|
71 |
||
5829 | 72 |
|
73 |
(* parse command *) |
|
74 |
||
6860 | 75 |
local |
6199 | 76 |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
77 |
fun terminate false = Scan.succeed () |
44357 | 78 |
| terminate true = |
79 |
Parse.group (fn () => "end of input") |
|
80 |
(Scan.option Parse.sync -- Parse.semicolon >> K ()); |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
81 |
|
26620 | 82 |
fun body cmd (name, _) = |
7026 | 83 |
(case cmd name of |
29311 | 84 |
SOME (Command {int_only, parse, ...}) => |
36950 | 85 |
Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only)) |
48191
c1def7433a72
internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
wenzelm
parents:
47416
diff
changeset
|
86 |
| NONE => |
c1def7433a72
internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
wenzelm
parents:
47416
diff
changeset
|
87 |
Scan.succeed (false, Toplevel.imperative (fn () => |
c1def7433a72
internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
wenzelm
parents:
47416
diff
changeset
|
88 |
error ("Bad parser for outer syntax command " ^ quote name)))); |
6860 | 89 |
|
90 |
in |
|
5829 | 91 |
|
26620 | 92 |
fun parse_command do_terminate cmd = |
36950 | 93 |
Parse.semicolon >> K NONE || |
94 |
Parse.sync >> K NONE || |
|
95 |
(Parse.position Parse.command :-- body cmd) --| terminate do_terminate |
|
6860 | 96 |
>> (fn ((name, pos), (int_only, f)) => |
15531 | 97 |
SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |> |
6860 | 98 |
Toplevel.interactive int_only |> f)); |
5829 | 99 |
|
6199 | 100 |
end; |
101 |
||
5829 | 102 |
|
43711 | 103 |
(* type outer_syntax *) |
104 |
||
105 |
datatype outer_syntax = Outer_Syntax of |
|
106 |
{commands: command Symtab.table, |
|
107 |
markups: (string * Thy_Output.markup) list}; |
|
108 |
||
109 |
fun make_outer_syntax commands markups = |
|
110 |
Outer_Syntax {commands = commands, markups = markups}; |
|
111 |
||
112 |
val empty_outer_syntax = make_outer_syntax Symtab.empty []; |
|
113 |
||
114 |
||
115 |
fun map_commands f (Outer_Syntax {commands, ...}) = |
|
116 |
let |
|
117 |
val commands' = f commands; |
|
118 |
val markups' = |
|
119 |
Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I) |
|
120 |
commands' []; |
|
121 |
in make_outer_syntax commands' markups' end; |
|
122 |
||
123 |
fun dest_commands (Outer_Syntax {commands, ...}) = |
|
50213 | 124 |
commands |> Symtab.dest |> sort_wrt #1; |
43711 | 125 |
|
126 |
fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands; |
|
127 |
||
128 |
fun is_markup (Outer_Syntax {markups, ...}) kind name = |
|
129 |
AList.lookup (op =) markups name = SOME kind; |
|
130 |
||
131 |
||
5829 | 132 |
|
9132 | 133 |
(** global outer syntax **) |
5829 | 134 |
|
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48638
diff
changeset
|
135 |
type command_spec = (string * Keyword.T) * Position.T; |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
136 |
|
7026 | 137 |
local |
138 |
||
43711 | 139 |
(*synchronized wrt. Keywords*) |
140 |
val global_outer_syntax = Unsynchronized.ref empty_outer_syntax; |
|
5952 | 141 |
|
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
142 |
fun add_command (name, kind) cmd = CRITICAL (fn () => |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
143 |
let |
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
144 |
val thy = ML_Context.the_global_context (); |
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
145 |
val Command {pos, ...} = cmd; |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
146 |
val _ = |
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
147 |
(case try (Thy_Header.the_keyword thy) name of |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
148 |
SOME spec => |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48771
diff
changeset
|
149 |
if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then () |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48638
diff
changeset
|
150 |
else error ("Inconsistent outer syntax keyword declaration " ^ |
48992 | 151 |
quote name ^ Position.here pos) |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
152 |
| NONE => |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
153 |
if Context.theory_name thy = Context.PureN |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
154 |
then Keyword.define (name, SOME kind) |
48992 | 155 |
else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos)); |
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
156 |
val _ = Position.report pos (command_markup true (name, cmd)); |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
157 |
in |
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
158 |
Unsynchronized.change global_outer_syntax (map_commands (fn commands => |
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
159 |
(if not (Symtab.defined commands name) then () |
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
160 |
else warning ("Redefining outer syntax command " ^ quote name); |
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
161 |
Symtab.update (name, cmd) commands))) |
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46876
diff
changeset
|
162 |
end); |
6722 | 163 |
|
7026 | 164 |
in |
165 |
||
43711 | 166 |
fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax)); |
7789 | 167 |
|
46970
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
168 |
fun check_syntax () = |
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
169 |
let |
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
170 |
val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_outer_syntax)); |
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
171 |
in |
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
172 |
(case subtract (op =) (map #1 (dest_commands syntax)) major of |
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
173 |
[] => () |
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
174 |
| missing => error ("Missing outer syntax command(s) " ^ commas_quote missing)) |
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
175 |
end; |
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset
|
176 |
|
43711 | 177 |
fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax); |
5829 | 178 |
|
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
179 |
fun command (spec, pos) comment parse = |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
180 |
add_command spec (new_command comment NONE false parse pos); |
24868 | 181 |
|
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
182 |
fun markup_command markup (spec, pos) comment parse = |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
183 |
add_command spec (new_command comment (SOME markup) false parse pos); |
7026 | 184 |
|
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
185 |
fun improper_command (spec, pos) comment parse = |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
186 |
add_command spec (new_command comment NONE true parse pos); |
29311 | 187 |
|
43711 | 188 |
end; |
189 |
||
5829 | 190 |
|
26990 | 191 |
(* local_theory commands *) |
192 |
||
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
193 |
fun local_theory_command do_print trans command_spec comment parse = |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
194 |
command command_spec comment (Parse.opt_target -- parse |
26990 | 195 |
>> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f)); |
196 |
||
29380 | 197 |
val local_theory' = local_theory_command false Toplevel.local_theory'; |
29311 | 198 |
val local_theory = local_theory_command false Toplevel.local_theory; |
26990 | 199 |
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof'; |
29311 | 200 |
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof; |
26990 | 201 |
|
202 |
||
24872 | 203 |
(* inspect syntax *) |
7026 | 204 |
|
50213 | 205 |
fun help_outer_syntax pats = |
206 |
dest_commands (#2 (get_syntax ())) |
|
207 |
|> filter (fn (name, _) => forall (fn pat => match_string pat name) pats) |
|
208 |
|> map pretty_command |
|
209 |
|> Pretty.chunks |> Pretty.writeln; |
|
210 |
||
9223 | 211 |
fun print_outer_syntax () = |
7026 | 212 |
let |
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
213 |
val ((keywords, _), outer_syntax) = |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
214 |
CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ()))); |
50213 | 215 |
val (int_cmds, cmds) = |
216 |
List.partition (fn (_, Command {int_only, ...}) => int_only) (dest_commands outer_syntax); |
|
7026 | 217 |
in |
43711 | 218 |
[Pretty.strs ("syntax keywords:" :: map quote keywords), |
50213 | 219 |
Pretty.big_list "commands:" (map pretty_command cmds), |
220 |
Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)] |
|
9223 | 221 |
|> Pretty.chunks |> Pretty.writeln |
7026 | 222 |
end; |
5829 | 223 |
|
224 |
||
225 |
||
9132 | 226 |
(** toplevel parsing **) |
5829 | 227 |
|
9132 | 228 |
(* basic sources *) |
6860 | 229 |
|
26620 | 230 |
fun toplevel_source term do_recover cmd src = |
9132 | 231 |
let |
232 |
val no_terminator = |
|
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset
|
233 |
Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof)); |
23682
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
234 |
fun recover int = |
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
235 |
(int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]); |
9132 | 236 |
in |
237 |
src |
|
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset
|
238 |
|> Token.source_proper |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset
|
239 |
|> Source.source Token.stopper |
36950 | 240 |
(Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME)) |
23682
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
241 |
(Option.map recover do_recover) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19060
diff
changeset
|
242 |
|> Source.map_filter I |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset
|
243 |
|> Source.source Token.stopper |
36950 | 244 |
(Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs)) |
23682
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
245 |
(Option.map recover do_recover) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19060
diff
changeset
|
246 |
|> Source.map_filter I |
9132 | 247 |
end; |
5829 | 248 |
|
7746 | 249 |
|
25580 | 250 |
(* off-line scanning/parsing *) |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
251 |
|
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
252 |
fun scan pos str = |
16195 | 253 |
Source.of_string str |
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
38422
diff
changeset
|
254 |
|> Symbol.source |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset
|
255 |
|> Token.source {do_recover = SOME false} Keyword.get_lexicons pos |
16195 | 256 |
|> Source.exhaust; |
257 |
||
25580 | 258 |
fun parse pos str = |
259 |
Source.of_string str |
|
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
38422
diff
changeset
|
260 |
|> Symbol.source |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset
|
261 |
|> Token.source {do_recover = SOME false} Keyword.get_lexicons pos |
43711 | 262 |
|> toplevel_source false NONE lookup_commands_dynamic |
25580 | 263 |
|> Source.exhaust; |
264 |
||
14091 | 265 |
|
24868 | 266 |
(* interactive source of toplevel transformers *) |
267 |
||
26600 | 268 |
type isar = |
269 |
(Toplevel.transition, (Toplevel.transition option, |
|
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset
|
270 |
(Token.T, (Token.T option, (Token.T, (Token.T, |
30573 | 271 |
(Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source) |
27770 | 272 |
Source.source) Source.source) Source.source) Source.source) |
273 |
Source.source) Source.source) Source.source) Source.source; |
|
26600 | 274 |
|
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
275 |
fun isar in_stream term : isar = |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
276 |
Source.tty in_stream |
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
38422
diff
changeset
|
277 |
|> Symbol.source |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset
|
278 |
|> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none |
43711 | 279 |
|> toplevel_source term (SOME true) lookup_commands_dynamic; |
24868 | 280 |
|
281 |
||
48918
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
282 |
(* side-comments *) |
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
283 |
|
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
284 |
local |
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
285 |
|
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
286 |
fun cmts (t1 :: t2 :: toks) = |
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
287 |
if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks |
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
288 |
else cmts (t2 :: toks) |
49564 | 289 |
| cmts _ = []; |
48918
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
290 |
|
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
291 |
in |
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
292 |
|
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
293 |
val span_cmts = filter Token.is_proper #> cmts; |
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
294 |
|
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
295 |
end; |
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
296 |
|
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48864
diff
changeset
|
297 |
|
44478
4fdb1009a370
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
wenzelm
parents:
44357
diff
changeset
|
298 |
(* read toplevel commands -- fail-safe *) |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
299 |
|
44658
5bec9c15ef29
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
wenzelm
parents:
44478
diff
changeset
|
300 |
fun read_span outer_syntax toks = |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
301 |
let |
43711 | 302 |
val commands = lookup_commands outer_syntax; |
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
303 |
|
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48768
diff
changeset
|
304 |
val proper_range = Position.set_range (Command.proper_range toks); |
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
305 |
val pos = |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
306 |
(case find_first Token.is_command toks of |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
307 |
SOME tok => Token.position_of tok |
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48768
diff
changeset
|
308 |
| NONE => proper_range); |
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
309 |
|
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
310 |
fun command_reports tok = |
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
311 |
if Token.is_command tok then |
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
312 |
let val name = Token.content_of tok in |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
313 |
(case commands name of |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
314 |
NONE => [] |
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48749
diff
changeset
|
315 |
| SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")]) |
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
316 |
end |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
317 |
else []; |
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
318 |
|
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
319 |
val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks; |
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48749
diff
changeset
|
320 |
val _ = Position.reports_text (token_reports @ maps command_reports toks); |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
321 |
in |
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
322 |
if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true) |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
323 |
else |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
324 |
(case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
325 |
[tr] => |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
326 |
if Keyword.is_control (Toplevel.name_of tr) then |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
327 |
(Toplevel.malformed pos "Illegal control command", true) |
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
328 |
else (tr, true) |
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48768
diff
changeset
|
329 |
| [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false) |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48768
diff
changeset
|
330 |
| _ => (Toplevel.malformed proper_range "Exactly one command expected", true)) |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48768
diff
changeset
|
331 |
handle ERROR msg => (Toplevel.malformed proper_range msg, true) |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
332 |
end; |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
333 |
|
44478
4fdb1009a370
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
wenzelm
parents:
44357
diff
changeset
|
334 |
fun read_element outer_syntax init {head, proof, proper_proof} = |
28436
4faf705a177d
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents:
28432
diff
changeset
|
335 |
let |
44658
5bec9c15ef29
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
wenzelm
parents:
44478
diff
changeset
|
336 |
val read = read_span outer_syntax o Thy_Syntax.span_content; |
5bec9c15ef29
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
wenzelm
parents:
44478
diff
changeset
|
337 |
val (tr, proper_head) = read head |>> Toplevel.modify_init init; |
5bec9c15ef29
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
wenzelm
parents:
44478
diff
changeset
|
338 |
val proof_trs = map read proof |> filter #2 |> map #1; |
28436
4faf705a177d
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents:
28432
diff
changeset
|
339 |
in |
47416 | 340 |
if proper_head andalso proper_proof andalso |
341 |
not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)] |
|
43621 | 342 |
else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs) |
28436
4faf705a177d
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents:
28432
diff
changeset
|
343 |
end; |
28432
944cb67f809a
load_thy: Toplevel.excursion based on units of command/proof pairs;
wenzelm
parents:
28424
diff
changeset
|
344 |
|
5829 | 345 |
end; |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
346 |