src/Pure/Thy/thy_header.scala
changeset 58861 5ff61774df11
parent 56823 37be55461dbe
child 58868 c5e1cce7ace3
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sat Nov 01 14:20:38 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Nov 01 15:01:41 2014 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    val BEGIN = "begin"
     1.5  
     1.6    private val lexicon =
     1.7 -    Scan.Lexicon("%", "(", ")", ",", "::", ";", "==",
     1.8 +    Scan.Lexicon("%", "(", ")", ",", "::", "==",
     1.9        AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY)
    1.10  
    1.11  
    1.12 @@ -75,8 +75,7 @@
    1.13        { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
    1.14  
    1.15      (keyword(HEADER) ~ tags) ~!
    1.16 -      ((document_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^
    1.17 -        { case _ ~ x => x } |
    1.18 +      ((document_source ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
    1.19      (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
    1.20    }
    1.21