equal
deleted
inserted
replaced
57 val _ = |
57 val _ = |
58 Theory.setup (add_presentation (fn {options, segments, ...} => fn thy => |
58 Theory.setup (add_presentation (fn {options, segments, ...} => fn thy => |
59 if exists (Toplevel.is_skipped_proof o #state) segments then () |
59 if exists (Toplevel.is_skipped_proof o #state) segments then () |
60 else |
60 else |
61 let |
61 let |
62 val body = Document_Output.present_thy options (Thy_Header.get_keywords thy) segments; |
62 val keywords = Thy_Header.get_keywords thy; |
|
63 val thy_name = Context.theory_name thy; |
|
64 val latex = Document_Output.present_thy options keywords thy_name segments; |
63 in |
65 in |
64 if Options.string options "document" = "false" then () |
66 if Options.string options "document" = "false" then () |
65 else |
67 else Export.export thy \<^path_binding>\<open>document/latex\<close> latex |
66 let |
|
67 val thy_name = Context.theory_name thy; |
|
68 val latex = Latex.isabelle_body thy_name body; |
|
69 in Export.export thy \<^path_binding>\<open>document/latex\<close> latex end |
|
70 end)); |
68 end)); |
71 |
69 |
72 |
70 |
73 |
71 |
74 (** thy database **) |
72 (** thy database **) |