tuned;
added sect, subsect, subsubsect;

--- a/src/Pure/Isar/isar_syn.ML	Tue Aug 03 19:04:02 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 03 19:04:20 1999 +0200
@@ -39,12 +39,6 @@
 
 (** formal comments **)
 
-val txtP = OuterSyntax.command "txt" "formal comment (proof)" K.prf_decl
-  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
-
-val textP = OuterSyntax.command "text" "formal comment (theory)" K.thy_decl
-  (P.comment >> (Toplevel.theory o IsarThy.add_text));
-
 val titleP = OuterSyntax.command "title" "document title" K.thy_heading
   ((P.comment -- Scan.optional P.comment Comment.none -- Scan.optional P.comment Comment.none)
     >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
@@ -61,6 +55,22 @@
 val subsubsectionP = OuterSyntax.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
+  (P.comment >> (Toplevel.theory o IsarThy.add_text));
+
+
+val sectP = OuterSyntax.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
+  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
+
+val subsubsectP = OuterSyntax.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
+  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
+
 
 
 (** theory sections **)
@@ -182,10 +192,6 @@
   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
     (Scan.succeed (Toplevel.theory PureThy.local_path));
 
-val pathP =
-  OuterSyntax.command "path" "modify name-space entry path" K.thy_decl
-    (P.xname >> (Toplevel.theory o Theory.add_path));
-
 
 (* use ML text *)
 
@@ -355,7 +361,7 @@
     (P.marg_comment >> IsarThy.default_proof);
 
 val skip_proofP =
-  OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
+  OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
     (P.marg_comment >> IsarThy.skip_proof);
 
 
@@ -548,22 +554,24 @@
   outer_parse.ML, otherwise be prepared for unexpected errors*)
 
 val keywords =
- ["!", "!!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<",
-  "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
+ ["!", "!!", "%", "%%", "(", ")", "*", "+", ",", "--", ":", "::", ";",
+  "<", "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
   "concl", "files", "infixl", "infixr", "is", "output", "{", "|",
   "}"];
 
 val parsers = [
   (*theory structure*)
   theoryP, end_excursionP, kill_excursionP, contextP,
+  (*formal comments*)
+  titleP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
+  sectP, subsectP, subsubsectP, txtP,
   (*theory sections*)
-  txtP, textP, titleP, chapterP, sectionP, subsectionP,
-  subsubsectionP, classesP, classrelP, defaultsortP, typedeclP,
-  typeabbrP, nontermP, aritiesP, constsP, syntaxP, translationsP,
-  axiomsP, defsP, constdefsP, theoremsP, lemmasP, globalP, localP,
-  pathP, useP, mlP, setupP, parse_ast_translationP,
-  parse_translationP, print_translationP, typed_print_translationP,
-  print_ast_translationP, token_translationP, oracleP,
+  classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
+  aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
+  constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP, setupP,
+  parse_ast_translationP, parse_translationP, print_translationP,
+  typed_print_translationP, print_ast_translationP,
+  token_translationP, oracleP,
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,

--- a/src/Pure/Isar/isar_thy.ML	Tue Aug 03 19:04:02 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Aug 03 19:04:20 1999 +0200
@@ -7,13 +7,16 @@
 
 signature ISAR_THY =
 sig
-  val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
-  val add_text: Comment.text -> theory -> theory
   val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
   val add_chapter: Comment.text -> theory -> theory
   val add_section: Comment.text -> theory -> theory
   val add_subsection: Comment.text -> theory -> theory
   val add_subsubsection: Comment.text -> theory -> theory
+  val add_text: Comment.text -> theory -> theory
+  val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T
+  val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T
+  val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
+  val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
   val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
   val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
@@ -157,7 +160,6 @@
 
 (* formal comments *)
 
-fun add_txt comment = ProofHistory.apply Proof.assert_forward;
 fun add_text comment thy = thy;
 fun add_title title author date thy = thy;
 val add_chapter = add_text;
@@ -165,6 +167,11 @@
 val add_subsection = add_text;
 val add_subsubsection = add_text;
 
+fun add_txt comment = ProofHistory.apply Proof.assert_forward;
+val add_sect = add_text;
+val add_subsect = add_text;
+val add_subsubsect = add_text;
+
 
 (* signature and syntax *)