51 |
51 |
52 fun add_presentation f = Presentation.map (cons (f, stamp ())); |
52 fun add_presentation f = Presentation.map (cons (f, stamp ())); |
53 |
53 |
54 val _ = |
54 val _ = |
55 Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => |
55 Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => |
|
56 (Present.export_html thy (map #span segments); |
56 if exists (Toplevel.is_skipped_proof o #state) segments then () |
57 if exists (Toplevel.is_skipped_proof o #state) segments then () |
57 else |
58 else |
58 let |
59 let |
59 val body = Thy_Output.present_thy options thy segments; |
60 val body = Thy_Output.present_thy options thy segments; |
60 in |
61 in |
61 if Options.string options "document" = "false" then () |
62 if Options.string options "document" = "false" then () |
62 else |
63 else |
63 let |
64 let |
64 val thy_name = Context.theory_name thy; |
65 val thy_name = Context.theory_name thy; |
65 val document_tex_name = Path.explode_binding0 ("document/" ^ thy_name ^ ".tex"); |
66 val document_tex_name = Present.document_tex_name thy; |
66 |
67 |
67 val latex = Latex.isabelle_body thy_name body; |
68 val latex = Latex.isabelle_body thy_name body; |
68 val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; |
69 val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; |
69 in Export.export thy document_tex_name (XML.blob output) end |
70 in Export.export thy document_tex_name (XML.blob output) end |
70 end)); |
71 end))); |
71 |
72 |
72 |
73 |
73 |
74 |
74 (** thy database **) |
75 (** thy database **) |
75 |
76 |
300 (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); |
301 (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); |
301 |
302 |
302 val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); |
303 val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); |
303 val elements = Thy_Element.parse_elements keywords spans; |
304 val elements = Thy_Element.parse_elements keywords spans; |
304 |
305 |
305 val symbols = Resources.html_symbols (); |
306 fun init () = Resources.begin_theory master_dir header parents; |
306 val html = implode (map (HTML.present_span symbols keywords) spans); |
|
307 |
|
308 fun init () = |
|
309 Resources.begin_theory master_dir header parents |
|
310 |> Present.begin_theory update_time html; |
|
311 |
|
312 val (results, thy) = |
307 val (results, thy) = |
313 cond_timeit true ("theory " ^ quote name) |
308 cond_timeit true ("theory " ^ quote name) |
314 (fn () => excursion keywords master_dir last_timing init elements); |
309 (fn () => excursion keywords master_dir last_timing init elements); |
315 |
310 |
316 fun present () = |
311 fun present () = |