author | haftmann |
Sun, 22 Feb 2009 18:00:05 +0100 | |
changeset 30060 | 672012330c4e |
parent 29428 | 3ab54b42ded8 |
child 30513 | 1796b8ea88aa |
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 |
|
29311 | 12 |
type 'a parser = 'a OuterParse.parser |
13 |
val command: string -> string -> OuterKeyword.T -> |
|
14 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
|
15 |
val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T -> |
|
16 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
|
17 |
val improper_command: string -> string -> OuterKeyword.T -> |
|
18 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
|
19 |
val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit |
|
29380 | 20 |
val local_theory': string -> string -> OuterKeyword.T -> |
21 |
(bool -> local_theory -> local_theory) parser -> unit |
|
26990 | 22 |
val local_theory: string -> string -> OuterKeyword.T -> |
29311 | 23 |
(local_theory -> local_theory) parser -> unit |
26990 | 24 |
val local_theory_to_proof': string -> string -> OuterKeyword.T -> |
29311 | 25 |
(bool -> local_theory -> Proof.state) parser -> unit |
26990 | 26 |
val local_theory_to_proof: string -> string -> OuterKeyword.T -> |
29311 | 27 |
(local_theory -> Proof.state) parser -> unit |
5883 | 28 |
val print_outer_syntax: unit -> unit |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
29 |
val scan: Position.T -> string -> OuterLex.token list |
25580 | 30 |
val parse: Position.T -> string -> Toplevel.transition list |
26431 | 31 |
val process_file: Path.T -> theory -> theory |
26600 | 32 |
type isar |
33 |
val isar: bool -> isar |
|
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
34 |
val prepare_command: Position.T -> string -> Toplevel.transition |
29428
3ab54b42ded8
load_thy: explicit after_load phase for presentation;
wenzelm
parents:
29380
diff
changeset
|
35 |
val load_thy: string -> Position.T -> string list -> bool -> unit -> unit |
5829 | 36 |
end; |
37 |
||
26600 | 38 |
structure OuterSyntax: OUTER_SYNTAX = |
5829 | 39 |
struct |
40 |
||
7750 | 41 |
structure T = OuterLex; |
6860 | 42 |
structure P = OuterParse; |
29311 | 43 |
type 'a parser = 'a P.parser; |
44 |
||
6860 | 45 |
|
5829 | 46 |
|
47 |
(** outer syntax **) |
|
48 |
||
29311 | 49 |
(* command parsers *) |
5829 | 50 |
|
29311 | 51 |
datatype command = Command of |
24868 | 52 |
{comment: string, |
53 |
markup: ThyOutput.markup option, |
|
54 |
int_only: bool, |
|
29311 | 55 |
parse: (Toplevel.transition -> Toplevel.transition) parser}; |
5829 | 56 |
|
29311 | 57 |
fun make_command comment markup int_only parse = |
58 |
Command {comment = comment, markup = markup, int_only = int_only, parse = parse}; |
|
5829 | 59 |
|
60 |
||
61 |
(* parse command *) |
|
62 |
||
6860 | 63 |
local |
6199 | 64 |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
65 |
fun terminate false = Scan.succeed () |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
66 |
| terminate true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ()); |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
67 |
|
26620 | 68 |
fun body cmd (name, _) = |
7026 | 69 |
(case cmd name of |
29311 | 70 |
SOME (Command {int_only, parse, ...}) => |
26620 | 71 |
P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only)) |
15531 | 72 |
| NONE => sys_error ("no parser for outer syntax command " ^ quote name)); |
6860 | 73 |
|
74 |
in |
|
5829 | 75 |
|
26620 | 76 |
fun parse_command do_terminate cmd = |
15531 | 77 |
P.semicolon >> K NONE || |
78 |
P.sync >> K NONE || |
|
26620 | 79 |
(P.position P.command :-- body cmd) --| terminate do_terminate |
6860 | 80 |
>> (fn ((name, pos), (int_only, f)) => |
15531 | 81 |
SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |> |
6860 | 82 |
Toplevel.interactive int_only |> f)); |
5829 | 83 |
|
6199 | 84 |
end; |
85 |
||
5829 | 86 |
|
87 |
||
9132 | 88 |
(** global outer syntax **) |
5829 | 89 |
|
7026 | 90 |
local |
91 |
||
29311 | 92 |
val global_commands = ref (Symtab.empty: command Symtab.table); |
22120 | 93 |
val global_markups = ref ([]: (string * ThyOutput.markup) list); |
5952 | 94 |
|
29311 | 95 |
fun change_commands f = CRITICAL (fn () => |
96 |
(change global_commands f; |
|
23939 | 97 |
global_markups := |
29311 | 98 |
Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I) |
99 |
(! global_commands) [])); |
|
6722 | 100 |
|
7026 | 101 |
in |
102 |
||
9132 | 103 |
(* access current syntax *) |
7026 | 104 |
|
29311 | 105 |
fun get_commands () = CRITICAL (fn () => ! global_commands); |
24868 | 106 |
fun get_markups () = CRITICAL (fn () => ! global_markups); |
7026 | 107 |
|
29311 | 108 |
fun get_command () = Symtab.lookup (get_commands ()); |
109 |
fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ())); |
|
7789 | 110 |
|
24868 | 111 |
fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind; |
5829 | 112 |
|
113 |
||
114 |
(* augment syntax *) |
|
115 |
||
29311 | 116 |
fun add_command name kind cmd = CRITICAL (fn () => |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
117 |
(OuterKeyword.command name kind; |
29311 | 118 |
if not (Symtab.defined (get_commands ()) name) then () |
24868 | 119 |
else warning ("Redefining outer syntax command " ^ quote name); |
29311 | 120 |
change_commands (Symtab.update (name, cmd)))); |
5829 | 121 |
|
24868 | 122 |
fun command name comment kind parse = |
29311 | 123 |
add_command name kind (make_command comment NONE false parse); |
5829 | 124 |
|
24868 | 125 |
fun markup_command markup name comment kind parse = |
29311 | 126 |
add_command name kind (make_command comment (SOME markup) false parse); |
24868 | 127 |
|
128 |
fun improper_command name comment kind parse = |
|
29311 | 129 |
add_command name kind (make_command comment NONE true parse); |
7026 | 130 |
|
131 |
end; |
|
5829 | 132 |
|
29311 | 133 |
fun internal_command name parse = |
134 |
command name "(internal)" OuterKeyword.control (parse >> (fn tr => Toplevel.no_timing o tr)); |
|
135 |
||
5829 | 136 |
|
26990 | 137 |
(* local_theory commands *) |
138 |
||
139 |
fun local_theory_command do_print trans name comment kind parse = |
|
140 |
command name comment kind (P.opt_target -- parse |
|
141 |
>> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f)); |
|
142 |
||
29380 | 143 |
val local_theory' = local_theory_command false Toplevel.local_theory'; |
29311 | 144 |
val local_theory = local_theory_command false Toplevel.local_theory; |
26990 | 145 |
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof'; |
29311 | 146 |
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof; |
26990 | 147 |
|
148 |
||
24872 | 149 |
(* inspect syntax *) |
7026 | 150 |
|
29311 | 151 |
fun dest_commands () = |
152 |
get_commands () |> Symtab.dest |> sort_wrt #1 |
|
153 |
|> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only)); |
|
5829 | 154 |
|
9223 | 155 |
fun print_outer_syntax () = |
7026 | 156 |
let |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
157 |
fun pretty_cmd (name, comment, _) = |
7026 | 158 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; |
29311 | 159 |
val (int_cmds, cmds) = List.partition #3 (dest_commands ()); |
7026 | 160 |
in |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
161 |
[Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())), |
18326 | 162 |
Pretty.big_list "commands:" (map pretty_cmd cmds), |
163 |
Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)] |
|
9223 | 164 |
|> Pretty.chunks |> Pretty.writeln |
7026 | 165 |
end; |
5829 | 166 |
|
167 |
||
168 |
||
9132 | 169 |
(** toplevel parsing **) |
5829 | 170 |
|
9132 | 171 |
(* basic sources *) |
6860 | 172 |
|
26620 | 173 |
fun toplevel_source term do_recover cmd src = |
9132 | 174 |
let |
175 |
val no_terminator = |
|
176 |
Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof)); |
|
23682
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
177 |
fun recover int = |
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
178 |
(int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]); |
9132 | 179 |
in |
180 |
src |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
181 |
|> T.source_proper |
9132 | 182 |
|> Source.source T.stopper |
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27855
diff
changeset
|
183 |
(Scan.bulk (P.$$$ "--" -- P.!!! P.doc_source >> K NONE || P.not_eof >> SOME)) |
23682
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
184 |
(Option.map recover do_recover) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19060
diff
changeset
|
185 |
|> Source.map_filter I |
24868 | 186 |
|> Source.source T.stopper |
26620 | 187 |
(Scan.bulk (fn xs => P.!!! (parse_command term (cmd ())) xs)) |
23682
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
188 |
(Option.map recover do_recover) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19060
diff
changeset
|
189 |
|> Source.map_filter I |
9132 | 190 |
end; |
5829 | 191 |
|
7746 | 192 |
|
25580 | 193 |
(* off-line scanning/parsing *) |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
194 |
|
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
195 |
fun scan pos str = |
16195 | 196 |
Source.of_string str |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
197 |
|> Symbol.source {do_recover = false} |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
198 |
|> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos |
16195 | 199 |
|> Source.exhaust; |
200 |
||
25580 | 201 |
fun parse pos str = |
202 |
Source.of_string str |
|
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
203 |
|> Symbol.source {do_recover = false} |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
204 |
|> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos |
29311 | 205 |
|> toplevel_source false NONE get_command |
25580 | 206 |
|> Source.exhaust; |
207 |
||
14091 | 208 |
|
26431 | 209 |
(* process file *) |
210 |
||
211 |
fun process_file path thy = |
|
212 |
let |
|
26881 | 213 |
val trs = parse (Path.position path) (File.read path); |
28424
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
214 |
val init = Toplevel.init_theory "" (K thy) (K ()) Toplevel.empty; |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
215 |
val result = fold Toplevel.command (init :: trs) Toplevel.toplevel; |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
216 |
in |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
217 |
(case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
218 |
(true, Context.Theory thy') => thy' |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
219 |
| _ => error "Bad result state: global theory expected") |
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset
|
220 |
end; |
26431 | 221 |
|
222 |
||
24868 | 223 |
(* interactive source of toplevel transformers *) |
224 |
||
26600 | 225 |
type isar = |
226 |
(Toplevel.transition, (Toplevel.transition option, |
|
227 |
(OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token, |
|
27770 | 228 |
(SymbolPos.T, Position.T * (Symbol.symbol, (string, unit) Source.source) |
229 |
Source.source) Source.source) Source.source) Source.source) |
|
230 |
Source.source) Source.source) Source.source) Source.source; |
|
26600 | 231 |
|
232 |
fun isar term : isar = |
|
24868 | 233 |
Source.tty |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
234 |
|> Symbol.source {do_recover = true} |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
235 |
|> T.source {do_recover = SOME true} OuterKeyword.get_lexicons Position.none |
29311 | 236 |
|> toplevel_source term (SOME true) get_command; |
24868 | 237 |
|
238 |
||
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
239 |
(* prepare toplevel commands -- fail-safe *) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
240 |
|
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
241 |
val not_singleton = "Exactly one command expected"; |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
242 |
|
29311 | 243 |
fun prepare_span commands span = |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
244 |
let |
29315
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
29311
diff
changeset
|
245 |
val range_pos = Position.encode_range (ThySyntax.span_range span); |
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
29311
diff
changeset
|
246 |
val toks = ThySyntax.span_content span; |
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
29311
diff
changeset
|
247 |
val _ = List.app ThySyntax.report_token toks; |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
248 |
in |
29311 | 249 |
(case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
250 |
[tr] => (tr, true) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
251 |
| [] => (Toplevel.ignored range_pos, false) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
252 |
| _ => (Toplevel.malformed range_pos not_singleton, true)) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
253 |
handle ERROR msg => (Toplevel.malformed range_pos msg, true) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
254 |
end; |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
255 |
|
29311 | 256 |
fun prepare_unit commands (cmd, proof, proper_proof) = |
28436
4faf705a177d
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents:
28432
diff
changeset
|
257 |
let |
29311 | 258 |
val (tr, proper_cmd) = prepare_span commands cmd; |
259 |
val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1; |
|
28436
4faf705a177d
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents:
28432
diff
changeset
|
260 |
in |
4faf705a177d
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents:
28432
diff
changeset
|
261 |
if proper_cmd andalso proper_proof then [(tr, proof_trs)] |
4faf705a177d
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents:
28432
diff
changeset
|
262 |
else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs) |
4faf705a177d
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents:
28432
diff
changeset
|
263 |
end; |
28432
944cb67f809a
load_thy: Toplevel.excursion based on units of command/proof pairs;
wenzelm
parents:
28424
diff
changeset
|
264 |
|
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
265 |
fun prepare_command pos str = |
29311 | 266 |
let val (lexs, commands) = get_syntax () in |
29315
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
29311
diff
changeset
|
267 |
(case ThySyntax.parse_spans lexs pos str of |
29311 | 268 |
[span] => #1 (prepare_span commands span) |
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
269 |
| _ => Toplevel.malformed pos not_singleton) |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
270 |
end; |
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
271 |
|
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
272 |
|
26611 | 273 |
(* load_thy *) |
7746 | 274 |
|
27839
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset
|
275 |
fun load_thy name pos text time = |
7683 | 276 |
let |
29311 | 277 |
val (lexs, commands) = get_syntax (); |
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
278 |
|
17932 | 279 |
val _ = Present.init_theory name; |
27855
b1bf607e06c2
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
wenzelm
parents:
27839
diff
changeset
|
280 |
|
29315
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
29311
diff
changeset
|
281 |
val toks = Source.exhausted (ThySyntax.token_source lexs pos (Source.of_list text)); |
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
29311
diff
changeset
|
282 |
val spans = Source.exhaust (ThySyntax.span_source toks); |
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
29311
diff
changeset
|
283 |
val _ = List.app ThySyntax.report_span spans; |
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
29311
diff
changeset
|
284 |
val units = Source.exhaust (ThySyntax.unit_source (Source.of_list spans)) |
29311 | 285 |
|> maps (prepare_unit commands); |
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
286 |
|
27855
b1bf607e06c2
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
wenzelm
parents:
27839
diff
changeset
|
287 |
val _ = Present.theory_source name |
29315
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
29311
diff
changeset
|
288 |
(fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans); |
27855
b1bf607e06c2
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
wenzelm
parents:
27839
diff
changeset
|
289 |
|
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
290 |
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); |
29428
3ab54b42ded8
load_thy: explicit after_load phase for presentation;
wenzelm
parents:
29380
diff
changeset
|
291 |
val results = cond_timeit time "" (fn () => Toplevel.excursion units); |
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
292 |
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); |
29428
3ab54b42ded8
load_thy: explicit after_load phase for presentation;
wenzelm
parents:
29380
diff
changeset
|
293 |
|
3ab54b42ded8
load_thy: explicit after_load phase for presentation;
wenzelm
parents:
29380
diff
changeset
|
294 |
fun after_load () = |
3ab54b42ded8
load_thy: explicit after_load phase for presentation;
wenzelm
parents:
29380
diff
changeset
|
295 |
ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup (Lazy.force results) toks |
3ab54b42ded8
load_thy: explicit after_load phase for presentation;
wenzelm
parents:
29380
diff
changeset
|
296 |
|> Buffer.content |
3ab54b42ded8
load_thy: explicit after_load phase for presentation;
wenzelm
parents:
29380
diff
changeset
|
297 |
|> Present.theory_output name; |
3ab54b42ded8
load_thy: explicit after_load phase for presentation;
wenzelm
parents:
29380
diff
changeset
|
298 |
in after_load end; |
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
299 |
|
5829 | 300 |
end; |