src/Pure/pure_syn.ML

--- a/src/Pure/pure_syn.ML	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/pure_syn.ML	Thu Nov 13 23:45:15 2014 +0100
@@ -8,24 +8,36 @@
 struct
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("header", @{here}) "theory header"
-    (Parse.document_source >> Thy_Output.header_markup);
+  Outer_Syntax.command ("header", @{here}) "theory header"
+    (Parse.document_source >> Thy_Output.old_header_command);
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("chapter", @{here}) "chapter heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
+  Outer_Syntax.command ("chapter", @{here}) "chapter heading"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+
+val _ =
+  Outer_Syntax.command ("section", @{here}) "section heading"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("section", @{here}) "section heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
+  Outer_Syntax.command ("subsection", @{here}) "subsection heading"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+
+val _ =
+  Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("subsection", @{here}) "subsection heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
+  Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("subsubsection", @{here}) "subsubsection heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
+  Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+
+val _ =
+  Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
+    (Parse.document_source >> K (Toplevel.imperative I));
 
 val _ =
   Outer_Syntax.command ("theory", @{here}) "begin theory"