equal
deleted
inserted
replaced
28 structure Thy_Info: THY_INFO = |
28 structure Thy_Info: THY_INFO = |
29 struct |
29 struct |
30 |
30 |
31 (** theory presentation **) |
31 (** theory presentation **) |
32 |
32 |
33 (* artefact names *) |
|
34 |
|
35 fun document_name ext thy = |
|
36 Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext); |
|
37 |
|
38 val document_tex_name = document_name "tex"; |
|
39 |
|
40 |
|
41 (* hook for consolidated theory *) |
33 (* hook for consolidated theory *) |
42 |
34 |
43 type presentation_context = |
35 type presentation_context = |
44 {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, |
36 {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, |
45 segments: Document_Output.segment list}; |
37 segments: Document_Output.segment list}; |
75 in |
67 in |
76 if Options.string options "document" = "false" then () |
68 if Options.string options "document" = "false" then () |
77 else |
69 else |
78 let |
70 let |
79 val thy_name = Context.theory_name thy; |
71 val thy_name = Context.theory_name thy; |
80 val document_tex_name = document_tex_name thy; |
|
81 val latex = Latex.isabelle_body thy_name body; |
72 val latex = Latex.isabelle_body thy_name body; |
82 in Export.export thy document_tex_name latex end |
73 in Export.export thy \<^path_binding>\<open>document/latex\<close> latex end |
83 end)); |
74 end)); |
84 |
75 |
85 |
76 |
86 |
77 |
87 (** thy database **) |
78 (** thy database **) |