Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/thy_header.ML
changeset 58861 5ff61774df11
parent 56801 8dd9df88f647
child 58863 64e571275b36 
--- a/src/Pure/Thy/thy_header.ML	Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sat Nov 01 15:01:41 2014 +0100
@@ -74,7 +74,7 @@
 
 val header_lexicons =
   pairself (Scan.make_lexicon o map Symbol.explode)
-   (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN],
+   (["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN],
     [headerN, theoryN]);
 
 
@@ -120,8 +120,7 @@
 
 val header =
   (Parse.command_name headerN -- Parse.tags) |--
-    (Parse.!!! (Parse.document_source -- Scan.repeat Parse.semicolon --
-      (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
+    (Parse.!!! (Parse.document_source -- (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
   (Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
 
 fun token_source pos str =
isabelle