# 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*)