# HG changeset patch
# User wenzelm
# Date 925488395 -7200
# Node ID de4047b0301736171d3e786a03b64c0bafaf7c6a
# Parent  68f950b1a6645d2d9344110b3bd31342c65af631
comment sections;
made "%" a keyword;

diff -r 68f950b1a664 -r de4047b03017 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 30 18:05:55 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 30 18:06:35 1999 +0200
@@ -43,23 +43,23 @@
 (* formal comments *)
 
 val textP = OuterSyntax.command "text" "formal comments"
-  (text >> (Toplevel.theory o IsarThy.add_text));
+  (comment >> (Toplevel.theory o IsarThy.add_text));
 
 val titleP = OuterSyntax.command "title" "document title"
-  ((text -- Scan.optional text "" -- Scan.optional text "")
+  ((comment -- Scan.optional comment Comment.empty -- Scan.optional comment Comment.empty)
     >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
 
 val chapterP = OuterSyntax.command "chapter" "chapter heading"
-  (text >> (Toplevel.theory o IsarThy.add_chapter));
+  (comment >> (Toplevel.theory o IsarThy.add_chapter));
 
 val sectionP = OuterSyntax.command "section" "section heading"
-  (text >> (Toplevel.theory o IsarThy.add_section));
+  (comment >> (Toplevel.theory o IsarThy.add_section));
 
 val subsectionP = OuterSyntax.command "subsection" "subsection heading"
-  (text >> (Toplevel.theory o IsarThy.add_subsection));
+  (comment >> (Toplevel.theory o IsarThy.add_subsection));
 
 val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading"
-  (text >> (Toplevel.theory o IsarThy.add_subsubsection));
+  (comment >> (Toplevel.theory o IsarThy.add_subsubsection));
 
 
 (* classes and sorts *)
@@ -493,9 +493,9 @@
   outer_parse.ML, otherwise be prepared for unexpected errors*)
 
 val keywords =
- ["!", "(", ")", "*", "+", "--", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
-  "?", "[", "]", "and", "as", "binder", "files", "infixl", "infixr",
-  "is", "output", "{", "|", "}"];
+ ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
+  "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "files",
+  "infixl", "infixr", "is", "output", "{", "|", "}"];
 
 val parsers = [
   (*theory structure*)