# HG changeset patch # User wenzelm # Date 1637666949 -3600 # Node ID c299abcf7081c53c6cb591a364767c652d500902 # Parent 32490add64b4cfb1bef72705aadca7666b4923ca clarified modules; diff -r 32490add64b4 -r c299abcf7081 src/Pure/Thy/document_output.ML --- a/src/Pure/Thy/document_output.ML Tue Nov 23 12:04:01 2021 +0100 +++ b/src/Pure/Thy/document_output.ML Tue Nov 23 12:29:09 2021 +0100 @@ -8,6 +8,10 @@ sig val document_reports: Input.source -> Position.report list val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text + val document_output: (xstring * Position.T) option * Input.source -> + Toplevel.transition -> Toplevel.transition + val document_output_markdown: (xstring * Position.T) option * Input.source -> + Toplevel.transition -> Toplevel.transition val check_comments: Proof.context -> Symbol_Pos.T list -> unit val output_token: Proof.context -> Token.T -> Latex.text val output_source: Proof.context -> string -> Latex.text @@ -111,6 +115,25 @@ in output_antiquotes ants end end; +fun document_output' markdown (loc, txt) = + let + fun output st = + let + val ctxt = Toplevel.presentation_context st; + val _ = Context_Position.reports ctxt (document_reports txt); + in output_document ctxt markdown txt end; + in + Toplevel.present (fn st => + (case loc of + NONE => output st + | SOME (_, pos) => + error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o + Toplevel.present_local_theory loc output + end; + +val document_output = document_output' {markdown = false}; +val document_output_markdown = document_output' {markdown = true}; + (* output tokens with formal comments *) diff -r 32490add64b4 -r c299abcf7081 src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Tue Nov 23 12:04:01 2021 +0100 +++ b/src/Pure/pure_syn.ML Tue Nov 23 12:29:09 2021 +0100 @@ -7,8 +7,6 @@ signature PURE_SYN = sig - val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source -> - Toplevel.transition -> Toplevel.transition val bootstrap_thy: theory end; @@ -17,56 +15,41 @@ val semi = Scan.option (Parse.$$$ ";"); -fun output_document state markdown txt = - let - val ctxt = Toplevel.presentation_context state; - val _ = Context_Position.reports ctxt (Document_Output.document_reports txt); - in Document_Output.output_document ctxt markdown txt end; - -fun document_command markdown (loc, txt) = - Toplevel.present (fn state => - (case loc of - NONE => output_document state markdown txt - | SOME (_, pos) => - error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o - Toplevel.present_local_theory loc (fn state => - output_document state markdown txt); - val _ = Outer_Syntax.command ("chapter", \<^here>) "chapter heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); + (Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); val _ = Outer_Syntax.command ("section", \<^here>) "section heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); + (Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); val _ = Outer_Syntax.command ("subsection", \<^here>) "subsection heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); + (Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); val _ = Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); + (Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); val _ = Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); + (Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); val _ = Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); + (Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); val _ = Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)" - (Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); + (Parse.opt_target -- Parse.document_source >> Document_Output.document_output_markdown); val _ = Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)" - (Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); + (Parse.opt_target -- Parse.document_source >> Document_Output.document_output_markdown); val _ = Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)" - (Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); + (Parse.opt_target -- Parse.document_source >> Document_Output.document_output_markdown); val _ = Outer_Syntax.command ("theory", \<^here>) "begin theory"