author  wenzelm 
Wed, 07 Jan 2009 12:08:22 +0100  
changeset 29380  a9ee3475abf4 
parent 29315  b074c05f00ad 
child 29428  3ab54b42ded8 
permissions  rwrr 
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 
0be8644c45eb
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
27831
diff
changeset

35 
val load_thy: string > Position.T > string list > bool > 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 "interactiveonly 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 
(* offline 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  failsafe *) 
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 (); 
25685  291 
val _ = cond_timeit time "" (fn () => 
28424
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset

292 
let 
28432
944cb67f809a
load_thy: Toplevel.excursion based on units of command/proof pairs;
wenzelm
parents:
28424
diff
changeset

293 
val (results, commit_exit) = Toplevel.excursion units; 
28424
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset

294 
val _ = 
28432
944cb67f809a
load_thy: Toplevel.excursion based on units of command/proof pairs;
wenzelm
parents:
28424
diff
changeset

295 
ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup results toks 
28424
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset

296 
> Buffer.content 
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset

297 
> Present.theory_output name 
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset

298 
val _ = commit_exit (); 
fc6ce1c4d5b7
simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents:
27872
diff
changeset

299 
in () end); 
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset

300 
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); 
24065  301 
in () end; 
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset

302 

5829  303 
end; 