# 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"