# HG changeset patch
# User wenzelm
# Date 921185616 -3600
# Node ID 5a76eb9030df187f2948955127a31d8c881e696a
# Parent  d015ccae03da3badd9aaecb8b2d0b8643baf419d
added 'title';
tuned names, comments;

diff -r d015ccae03da -r 5a76eb9030df src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 11 21:52:49 1999 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 11 21:53:36 1999 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Pure outer syntax.
+Isar/Pure outer syntax.
 
 TODO:
   - add_parsers: warn if command name coincides with other keyword (if
@@ -15,7 +15,7 @@
   - check evaluation of transformers (exns!);
   - 'result' command;
   - '--' (comment) option almost everywhere:
-  - 'thm': xthms1;
+  - 'thms': xthms1 (vs. 'thm' (!?));
 *)
 
 signature ISAR_SYN =
@@ -58,6 +58,10 @@
 val textP = OuterSyntax.parser false "text" "formal comments"
   (text >> (Toplevel.theory o IsarThy.add_text));
 
+val titleP = OuterSyntax.parser false "title" "document title"
+  ((text -- Scan.optional text "" -- Scan.optional text "")
+    >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
+
 val chapterP = OuterSyntax.parser false "chapter" "chapter heading"
   (text >> (Toplevel.theory o IsarThy.add_chapter));
 
@@ -90,7 +94,7 @@
 (* types *)
 
 val typedeclP =
-  OuterSyntax.parser false "typedecl" "declare logical type"
+  OuterSyntax.parser false "typedecl" "Pure type declaration"
     (type_args -- name -- opt_infix
       >> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
 
@@ -452,7 +456,7 @@
     (term >> IsarCmd.print_term);
 
 val print_typeP =
-  OuterSyntax.parser true "typ" "read and print type"
+  OuterSyntax.parser true "type" "read and print type"
     (typ >> IsarCmd.print_type);
 
 
@@ -518,7 +522,7 @@
   (*theory structure*)
   theoryP, endP, contextP, update_contextP,
   (*theory sections*)
-  textP, chapterP, sectionP, subsectionP, subsubsectionP, classesP,
+  textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP, classesP,
   classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, aritiesP,
   constsP, syntaxP, translationsP, axiomsP, defsP, theoremsP, lemmasP,
   axclassP, instanceP, globalP, localP, pathP, useP, mlP, setupP,