15 structure Pure_Syn: PURE_SYN = |
15 structure Pure_Syn: PURE_SYN = |
16 struct |
16 struct |
17 |
17 |
18 val semi = Scan.option (Parse.$$$ ";"); |
18 val semi = Scan.option (Parse.$$$ ";"); |
19 |
19 |
20 fun document_command {markdown} (loc, txt) = |
20 fun output_document state markdown txt = |
|
21 let |
|
22 val ctxt = Toplevel.presentation_context state; |
|
23 val _ = |
|
24 Context_Position.report ctxt |
|
25 (Input.pos_of txt) (Markup.language_document (Input.is_delimited txt)); |
|
26 in Thy_Output.output_document ctxt markdown txt end; |
|
27 |
|
28 fun document_command markdown (loc, txt) = |
21 Toplevel.keep (fn state => |
29 Toplevel.keep (fn state => |
22 (case loc of |
30 (case loc of |
23 NONE => |
31 NONE => ignore (output_document state markdown txt) |
24 ignore (Thy_Output.output_text |
|
25 (Toplevel.presentation_context state) {markdown = markdown} txt) |
|
26 | SOME (_, pos) => |
32 | SOME (_, pos) => |
27 error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o |
33 error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o |
28 Toplevel.present_local_theory loc (fn state => |
34 Toplevel.present_local_theory loc (fn state => |
29 ignore (Thy_Output.output_text (Toplevel.presentation_context state) {markdown = markdown} txt)); |
35 ignore (output_document state markdown txt)); |
30 |
36 |
31 val _ = |
37 val _ = |
32 Outer_Syntax.command ("chapter", \<^here>) "chapter heading" |
38 Outer_Syntax.command ("chapter", \<^here>) "chapter heading" |
33 (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
39 (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
34 |
40 |