src/Pure/pure_syn.ML

--- a/src/Pure/pure_syn.ML	Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/pure_syn.ML	Mon Jan 08 23:45:43 2018 +0100
@@ -7,6 +7,8 @@
 
 signature PURE_SYN =
 sig
+  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
+    Toplevel.transition -> Toplevel.transition
   val bootstrap_thy: theory
 end;
 
@@ -15,47 +17,52 @@
 
 val semi = Scan.option (Parse.$$$ ";");
 
+fun document_command {markdown} (loc, txt) =
+  Toplevel.keep (fn state =>
+    (case loc of
+      NONE =>
+        ignore (Thy_Output.output_text
+          (Toplevel.presentation_context state) {markdown = markdown} txt)
+    | SOME (_, pos) =>
+        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
+  Toplevel.present_local_theory loc (fn state =>
+    ignore (Thy_Output.output_text (Toplevel.presentation_context state) {markdown = markdown} txt));
+
 val _ =
   Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("section", \<^here>) "section heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
-    (Parse.opt_target -- Parse.document_source --| semi
-      >> Thy_Output.document_command {markdown = false});
+    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
+    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
 
 val _ =
   Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
+    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
 
 val _ =
   Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
+    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
 
 val _ =
   Outer_Syntax.command ("theory", \<^here>) "begin theory"