src/Pure/Thy/thy_header.scala
changeset 58868 c5e1cce7ace3
parent 58861 5ff61774df11
child 58899 0a793c580685
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sun Nov 02 13:26:20 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Nov 02 15:27:37 2014 +0100
     1.3 @@ -16,6 +16,11 @@
     1.4  object Thy_Header extends Parse.Parser
     1.5  {
     1.6    val HEADER = "header"
     1.7 +  val CHAPTER = "chapter"
     1.8 +  val SECTION = "section"
     1.9 +  val SUBSECTION = "subsection"
    1.10 +  val SUBSUBSECTION = "subsubsection"
    1.11 +
    1.12    val THEORY = "theory"
    1.13    val IMPORTS = "imports"
    1.14    val KEYWORDS = "keywords"
    1.15 @@ -23,8 +28,8 @@
    1.16    val BEGIN = "begin"
    1.17  
    1.18    private val lexicon =
    1.19 -    Scan.Lexicon("%", "(", ")", ",", "::", "==",
    1.20 -      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY)
    1.21 +    Scan.Lexicon("%", "(", ")", ",", "::", "==", AND, BEGIN,
    1.22 +      HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY)
    1.23  
    1.24  
    1.25    /* theory file name */
    1.26 @@ -74,9 +79,15 @@
    1.27        keyword(BEGIN) ^^
    1.28        { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
    1.29  
    1.30 -    (keyword(HEADER) ~ tags) ~!
    1.31 -      ((document_source ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
    1.32 -    (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
    1.33 +    val heading =
    1.34 +      (keyword(HEADER) |
    1.35 +        keyword(CHAPTER) |
    1.36 +        keyword(SECTION) |
    1.37 +        keyword(SUBSECTION) |
    1.38 +        keyword(SUBSUBSECTION)) ~
    1.39 +      tags ~! document_source
    1.40 +
    1.41 +    (rep(heading) ~ keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
    1.42    }
    1.43  
    1.44