comment sections;
authorwenzelm
Fri Apr 30 18:06:35 1999 +0200 (1999-04-30 ago)
changeset 6551de4047b03017
parent 6550 68f950b1a664
child 6552 28553eba1913
comment sections;
made "%" a keyword;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 30 18:05:55 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 30 18:06:35 1999 +0200
     1.3 @@ -43,23 +43,23 @@
     1.4  (* formal comments *)
     1.5  
     1.6  val textP = OuterSyntax.command "text" "formal comments"
     1.7 -  (text >> (Toplevel.theory o IsarThy.add_text));
     1.8 +  (comment >> (Toplevel.theory o IsarThy.add_text));
     1.9  
    1.10  val titleP = OuterSyntax.command "title" "document title"
    1.11 -  ((text -- Scan.optional text "" -- Scan.optional text "")
    1.12 +  ((comment -- Scan.optional comment Comment.empty -- Scan.optional comment Comment.empty)
    1.13      >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    1.14  
    1.15  val chapterP = OuterSyntax.command "chapter" "chapter heading"
    1.16 -  (text >> (Toplevel.theory o IsarThy.add_chapter));
    1.17 +  (comment >> (Toplevel.theory o IsarThy.add_chapter));
    1.18  
    1.19  val sectionP = OuterSyntax.command "section" "section heading"
    1.20 -  (text >> (Toplevel.theory o IsarThy.add_section));
    1.21 +  (comment >> (Toplevel.theory o IsarThy.add_section));
    1.22  
    1.23  val subsectionP = OuterSyntax.command "subsection" "subsection heading"
    1.24 -  (text >> (Toplevel.theory o IsarThy.add_subsection));
    1.25 +  (comment >> (Toplevel.theory o IsarThy.add_subsection));
    1.26  
    1.27  val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading"
    1.28 -  (text >> (Toplevel.theory o IsarThy.add_subsubsection));
    1.29 +  (comment >> (Toplevel.theory o IsarThy.add_subsubsection));
    1.30  
    1.31  
    1.32  (* classes and sorts *)
    1.33 @@ -493,9 +493,9 @@
    1.34    outer_parse.ML, otherwise be prepared for unexpected errors*)
    1.35  
    1.36  val keywords =
    1.37 - ["!", "(", ")", "*", "+", "--", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
    1.38 -  "?", "[", "]", "and", "as", "binder", "files", "infixl", "infixr",
    1.39 -  "is", "output", "{", "|", "}"];
    1.40 + ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
    1.41 +  "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "files",
    1.42 +  "infixl", "infixr", "is", "output", "{", "|", "}"];
    1.43  
    1.44  val parsers = [
    1.45    (*theory structure*)