# HG changeset patch
# User wenzelm
# Date 939162773 -7200
# Node ID dfb8beddbefedb3baffe53af0f3f104b5e9ce4b4
# Parent  5b9c45b217820e05ef1d4258ee59f3f7a8fb2852
OuterSyntax.markup_command;

diff -r 5b9c45b21782 -r dfb8beddbefe src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Oct 06 00:31:40 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 06 00:32:53 1999 +0200
@@ -37,37 +37,38 @@
 
 
 
-(** formal comments **)
+(** markup commands **)
 
-val headerP = OuterSyntax.command "header" "theory header" K.diag
+val headerP = OuterSyntax.markup_command "header" "theory header" K.diag
   (P.comment >> IsarThy.add_header);
 
-val chapterP = OuterSyntax.command "chapter" "chapter heading" K.thy_heading
+val chapterP = OuterSyntax.markup_command "chapter" "chapter heading" K.thy_heading
   (P.comment >> (Toplevel.theory o IsarThy.add_chapter));
 
-val sectionP = OuterSyntax.command "section" "section heading" K.thy_heading
+val sectionP = OuterSyntax.markup_command "section" "section heading" K.thy_heading
   (P.comment >> (Toplevel.theory o IsarThy.add_section));
 
-val subsectionP = OuterSyntax.command "subsection" "subsection heading" K.thy_heading
+val subsectionP = OuterSyntax.markup_command "subsection" "subsection heading" K.thy_heading
   (P.comment >> (Toplevel.theory o IsarThy.add_subsection));
 
-val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading" K.thy_heading
-  (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
+val subsubsectionP =
+  OuterSyntax.markup_command "subsubsection" "subsubsection heading" K.thy_heading
+    (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
 
-val textP = OuterSyntax.command "text" "formal comment (theory)" K.thy_decl
+val textP = OuterSyntax.markup_command "text" "formal comment (theory)" K.thy_decl
   (P.comment >> (Toplevel.theory o IsarThy.add_text));
 
 
-val sectP = OuterSyntax.command "sect" "formal comment (proof)" K.prf_decl
+val sectP = OuterSyntax.markup_command "sect" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
 
-val subsectP = OuterSyntax.command "subsect" "formal comment (proof)" K.prf_decl
+val subsectP = OuterSyntax.markup_command "subsect" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
 
-val subsubsectP = OuterSyntax.command "subsubsect" "formal comment (proof)" K.prf_decl
+val subsubsectP = OuterSyntax.markup_command "subsubsect" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
 
-val txtP = OuterSyntax.command "txt" "formal comment (proof)" K.prf_decl
+val txtP = OuterSyntax.markup_command "txt" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));