equal
deleted
inserted
replaced
54 val extend = I; |
54 val extend = I; |
55 fun merge data : T = Library.merge (eq_snd op =) data; |
55 fun merge data : T = Library.merge (eq_snd op =) data; |
56 ); |
56 ); |
57 |
57 |
58 fun apply_presentation (context: presentation_context) thy = |
58 fun apply_presentation (context: presentation_context) thy = |
59 ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); |
59 (ignore (Par_List.map (fn (f, _) => f context thy (Presentation.get thy))); |
|
60 Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) []); |
60 |
61 |
61 fun add_presentation f = Presentation.map (cons (f, stamp ())); |
62 fun add_presentation f = Presentation.map (cons (f, stamp ())); |
62 |
63 |
63 val _ = |
64 val _ = |
64 Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => |
65 Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => |
65 (Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) []; |
|
66 if exists (Toplevel.is_skipped_proof o #state) segments then () |
66 if exists (Toplevel.is_skipped_proof o #state) segments then () |
67 else |
67 else |
68 let |
68 let |
69 val body = Thy_Output.present_thy options thy segments; |
69 val body = Thy_Output.present_thy options thy segments; |
70 in |
70 in |
75 val document_tex_name = document_tex_name thy; |
75 val document_tex_name = document_tex_name thy; |
76 |
76 |
77 val latex = Latex.isabelle_body thy_name body; |
77 val latex = Latex.isabelle_body thy_name body; |
78 val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; |
78 val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; |
79 in Export.export thy document_tex_name (XML.blob output) end |
79 in Export.export thy document_tex_name (XML.blob output) end |
80 end))); |
80 end)); |
81 |
81 |
82 |
82 |
83 |
83 |
84 (** thy database **) |
84 (** thy database **) |
85 |
85 |