author | wenzelm |
Fri, 08 Jul 2011 21:44:47 +0200 | |
changeset 43712 | 3c2c912af2ef |
parent 43711 | 608d1b451f67 |
child 44186 | 806f0ec1a43d |
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 |
36950 | 15 |
val command: string -> string -> Keyword.T -> |
29311 | 16 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36959
diff
changeset
|
17 |
val markup_command: Thy_Output.markup -> string -> string -> Keyword.T -> |
29311 | 18 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
36950 | 19 |
val improper_command: string -> string -> Keyword.T -> |
29311 | 20 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
43711 | 21 |
val internal_command: string -> |
22 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
|
36950 | 23 |
val local_theory': string -> string -> Keyword.T -> |
29380 | 24 |
(bool -> local_theory -> local_theory) parser -> unit |
36950 | 25 |
val local_theory: string -> string -> Keyword.T -> |
29311 | 26 |
(local_theory -> local_theory) parser -> unit |
36950 | 27 |
val local_theory_to_proof': string -> string -> Keyword.T -> |
29311 | 28 |
(bool -> local_theory -> Proof.state) parser -> unit |
36950 | 29 |
val local_theory_to_proof: string -> string -> Keyword.T -> |
29311 | 30 |
(local_theory -> Proof.state) parser -> unit |
5883 | 31 |
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
|
32 |
val scan: Position.T -> string -> Token.T list |
25580 | 33 |
val parse: Position.T -> string -> Toplevel.transition list |
26431 | 34 |
val process_file: Path.T -> theory -> theory |
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 |
43712
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43711
diff
changeset
|
37 |
val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool |
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43711
diff
changeset
|
38 |
val prepare_element: outer_syntax -> (Path.T option -> theory) -> Thy_Syntax.element -> |
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43711
diff
changeset
|
39 |
(Toplevel.transition * Toplevel.transition list) list |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
40 |
val prepare_command: Position.T -> string -> Toplevel.transition |
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, |
29311 | 54 |
parse: (Toplevel.transition -> Toplevel.transition) parser}; |
5829 | 55 |
|
29311 | 56 |
fun make_command comment markup int_only parse = |
57 |
Command {comment = comment, markup = markup, int_only = int_only, parse = parse}; |
|
5829 | 58 |
|
59 |
||
60 |
(* parse command *) |
|
61 |
||
6860 | 62 |
local |
6199 | 63 |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
64 |
fun terminate false = Scan.succeed () |
36950 | 65 |
| terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ()); |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
66 |
|
26620 | 67 |
fun body cmd (name, _) = |
7026 | 68 |
(case cmd name of |
29311 | 69 |
SOME (Command {int_only, parse, ...}) => |
36950 | 70 |
Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only)) |
37852
a902f158b4fc
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
wenzelm
parents:
37713
diff
changeset
|
71 |
| NONE => raise Fail ("No parser for outer syntax command " ^ quote name)); |
6860 | 72 |
|
73 |
in |
|
5829 | 74 |
|
26620 | 75 |
fun parse_command do_terminate cmd = |
36950 | 76 |
Parse.semicolon >> K NONE || |
77 |
Parse.sync >> K NONE || |
|
78 |
(Parse.position Parse.command :-- body cmd) --| terminate do_terminate |
|
6860 | 79 |
>> (fn ((name, pos), (int_only, f)) => |
15531 | 80 |
SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |> |
6860 | 81 |
Toplevel.interactive int_only |> f)); |
5829 | 82 |
|
6199 | 83 |
end; |
84 |
||
5829 | 85 |
|
43711 | 86 |
(* type outer_syntax *) |
87 |
||
88 |
datatype outer_syntax = Outer_Syntax of |
|
89 |
{commands: command Symtab.table, |
|
90 |
markups: (string * Thy_Output.markup) list}; |
|
91 |
||
92 |
fun make_outer_syntax commands markups = |
|
93 |
Outer_Syntax {commands = commands, markups = markups}; |
|
94 |
||
95 |
val empty_outer_syntax = make_outer_syntax Symtab.empty []; |
|
96 |
||
97 |
||
98 |
fun map_commands f (Outer_Syntax {commands, ...}) = |
|
99 |
let |
|
100 |
val commands' = f commands; |
|
101 |
val markups' = |
|
102 |
Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I) |
|
103 |
commands' []; |
|
104 |
in make_outer_syntax commands' markups' end; |
|
105 |
||
106 |
fun dest_commands (Outer_Syntax {commands, ...}) = |
|
107 |
commands |> Symtab.dest |> sort_wrt #1 |
|
108 |
|> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only)); |
|
109 |
||
110 |
fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands; |
|
111 |
||
112 |
fun is_markup (Outer_Syntax {markups, ...}) kind name = |
|
113 |
AList.lookup (op =) markups name = SOME kind; |
|
114 |
||
115 |
||
5829 | 116 |
|
9132 | 117 |
(** global outer syntax **) |
5829 | 118 |
|
7026 | 119 |
local |
120 |
||
43711 | 121 |
(*synchronized wrt. Keywords*) |
122 |
val global_outer_syntax = Unsynchronized.ref empty_outer_syntax; |
|
5952 | 123 |
|
43711 | 124 |
fun add_command name kind cmd = CRITICAL (fn () => |
125 |
(Keyword.command name kind; |
|
126 |
Unsynchronized.change global_outer_syntax (map_commands (fn commands => |
|
127 |
(if not (Symtab.defined commands name) then () |
|
128 |
else warning ("Redefining outer syntax command " ^ quote name); |
|
129 |
Symtab.update (name, cmd) commands))))); |
|
6722 | 130 |
|
7026 | 131 |
in |
132 |
||
43711 | 133 |
fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax)); |
7789 | 134 |
|
43711 | 135 |
fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax); |
5829 | 136 |
|
24868 | 137 |
fun command name comment kind parse = |
29311 | 138 |
add_command name kind (make_command comment NONE false parse); |
5829 | 139 |
|
24868 | 140 |
fun markup_command markup name comment kind parse = |
29311 | 141 |
add_command name kind (make_command comment (SOME markup) false parse); |
24868 | 142 |
|
143 |
fun improper_command name comment kind parse = |
|
29311 | 144 |
add_command name kind (make_command comment NONE true parse); |
7026 | 145 |
|
29311 | 146 |
fun internal_command name parse = |
36950 | 147 |
command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr)); |
29311 | 148 |
|
43711 | 149 |
end; |
150 |
||
5829 | 151 |
|
26990 | 152 |
(* local_theory commands *) |
153 |
||
154 |
fun local_theory_command do_print trans name comment kind parse = |
|
36950 | 155 |
command name comment kind (Parse.opt_target -- parse |
26990 | 156 |
>> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f)); |
157 |
||
29380 | 158 |
val local_theory' = local_theory_command false Toplevel.local_theory'; |
29311 | 159 |
val local_theory = local_theory_command false Toplevel.local_theory; |
26990 | 160 |
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof'; |
29311 | 161 |
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof; |
26990 | 162 |
|
163 |
||
24872 | 164 |
(* inspect syntax *) |
7026 | 165 |
|
9223 | 166 |
fun print_outer_syntax () = |
7026 | 167 |
let |
43711 | 168 |
val (keywords, outer_syntax) = |
169 |
CRITICAL (fn () => (Keyword.dest_keywords (), #2 (get_syntax ()))); |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
170 |
fun pretty_cmd (name, comment, _) = |
7026 | 171 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; |
43711 | 172 |
val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax); |
7026 | 173 |
in |
43711 | 174 |
[Pretty.strs ("syntax keywords:" :: map quote keywords), |
18326 | 175 |
Pretty.big_list "commands:" (map pretty_cmd cmds), |
176 |
Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)] |
|
9223 | 177 |
|> Pretty.chunks |> Pretty.writeln |
7026 | 178 |
end; |
5829 | 179 |
|
180 |
||
181 |
||
9132 | 182 |
(** toplevel parsing **) |
5829 | 183 |
|
9132 | 184 |
(* basic sources *) |
6860 | 185 |
|
26620 | 186 |
fun toplevel_source term do_recover cmd src = |
9132 | 187 |
let |
188 |
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
|
189 |
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
|
190 |
fun recover int = |
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
191 |
(int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]); |
9132 | 192 |
in |
193 |
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
|
194 |
|> 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
|
195 |
|> Source.source Token.stopper |
36950 | 196 |
(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
|
197 |
(Option.map recover do_recover) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19060
diff
changeset
|
198 |
|> 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
|
199 |
|> Source.source Token.stopper |
36950 | 200 |
(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
|
201 |
(Option.map recover do_recover) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19060
diff
changeset
|
202 |
|> Source.map_filter I |
9132 | 203 |
end; |
5829 | 204 |
|
7746 | 205 |
|
25580 | 206 |
(* off-line scanning/parsing *) |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
207 |
|
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
208 |
fun scan pos str = |
16195 | 209 |
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
|
210 |
|> 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
|
211 |
|> Token.source {do_recover = SOME false} Keyword.get_lexicons pos |
16195 | 212 |
|> Source.exhaust; |
213 |
||
25580 | 214 |
fun parse pos str = |
215 |
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
|
216 |
|> 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
|
217 |
|> Token.source {do_recover = SOME false} Keyword.get_lexicons pos |
43711 | 218 |
|> toplevel_source false NONE lookup_commands_dynamic |
25580 | 219 |
|> Source.exhaust; |
220 |
||
14091 | 221 |
|
26431 | 222 |
(* process file *) |
223 |
||
224 |
fun process_file path thy = |
|
225 |
let |
|
26881 | 226 |
val trs = parse (Path.position path) (File.read path); |
41536
47fef6afe756
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents:
41484
diff
changeset
|
227 |
val init = Toplevel.init_theory NONE "" (K thy) Toplevel.empty; |
28424
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
228 |
val result = fold Toplevel.command (init :: trs) Toplevel.toplevel; |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
229 |
in |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
230 |
(case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
231 |
(true, Context.Theory thy') => thy' |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
232 |
| _ => error "Bad result state: global theory expected") |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
233 |
end; |
26431 | 234 |
|
235 |
||
24868 | 236 |
(* interactive source of toplevel transformers *) |
237 |
||
26600 | 238 |
type isar = |
239 |
(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
|
240 |
(Token.T, (Token.T option, (Token.T, (Token.T, |
30573 | 241 |
(Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source) |
27770 | 242 |
Source.source) Source.source) Source.source) Source.source) |
243 |
Source.source) Source.source) Source.source) Source.source; |
|
26600 | 244 |
|
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
245 |
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
|
246 |
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
|
247 |
|> 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
|
248 |
|> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none |
43711 | 249 |
|> toplevel_source term (SOME true) lookup_commands_dynamic; |
24868 | 250 |
|
251 |
||
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
252 |
(* prepare toplevel commands -- fail-safe *) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
253 |
|
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
254 |
val not_singleton = "Exactly one command expected"; |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
255 |
|
43711 | 256 |
fun prepare_span outer_syntax span = |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
257 |
let |
43711 | 258 |
val commands = lookup_commands outer_syntax; |
41484 | 259 |
val range_pos = Position.set_range (Thy_Syntax.span_range span); |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36959
diff
changeset
|
260 |
val toks = Thy_Syntax.span_content span; |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36959
diff
changeset
|
261 |
val _ = List.app Thy_Syntax.report_token toks; |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
262 |
in |
29311 | 263 |
(case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of |
37713
c82cf6e11669
Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
wenzelm
parents:
37216
diff
changeset
|
264 |
[tr] => |
c82cf6e11669
Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
wenzelm
parents:
37216
diff
changeset
|
265 |
if Keyword.is_control (Toplevel.name_of tr) then |
c82cf6e11669
Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
wenzelm
parents:
37216
diff
changeset
|
266 |
(Toplevel.malformed range_pos "Illegal control command", true) |
c82cf6e11669
Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
wenzelm
parents:
37216
diff
changeset
|
267 |
else (tr, true) |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
268 |
| [] => (Toplevel.ignored range_pos, false) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
269 |
| _ => (Toplevel.malformed range_pos not_singleton, true)) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
270 |
handle ERROR msg => (Toplevel.malformed range_pos msg, true) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
271 |
end; |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
272 |
|
43711 | 273 |
fun prepare_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
|
274 |
let |
43711 | 275 |
val (tr, proper_head) = prepare_span outer_syntax head |>> Toplevel.modify_init init; |
276 |
val proof_trs = map (prepare_span outer_syntax) proof |> filter #2 |> map #1; |
|
28436
4faf705a177d
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents:
28432
diff
changeset
|
277 |
in |
43621 | 278 |
if proper_head andalso proper_proof then [(tr, proof_trs)] |
279 |
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
|
280 |
end; |
28432
944cb67f809a
load_thy: Toplevel.excursion based on units of command/proof pairs;
wenzelm
parents:
28424
diff
changeset
|
281 |
|
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
282 |
fun prepare_command pos str = |
43711 | 283 |
let val (lexs, outer_syntax) = get_syntax () in |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36959
diff
changeset
|
284 |
(case Thy_Syntax.parse_spans lexs pos str of |
43711 | 285 |
[span] => #1 (prepare_span outer_syntax span) |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
286 |
| _ => Toplevel.malformed pos not_singleton) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
287 |
end; |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
288 |
|
5829 | 289 |
end; |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
290 |