src/Pure/Thy/thy_header.scala
changeset 58999 ed09ae4ea2d8
parent 58928 23d0ffd48006
child 59694 d2bb4b5ed862
     1.1 --- a/src/Pure/Thy/thy_header.scala	Thu Nov 13 17:28:11 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Nov 13 23:45:15 2014 +0100
     1.3 @@ -24,6 +24,9 @@
     1.4    val SECTION = "section"
     1.5    val SUBSECTION = "subsection"
     1.6    val SUBSUBSECTION = "subsubsection"
     1.7 +  val TEXT = "text"
     1.8 +  val TXT = "txt"
     1.9 +  val TEXT_RAW = "text_raw"
    1.10  
    1.11    val THEORY = "theory"
    1.12    val IMPORTS = "imports"
    1.13 @@ -43,11 +46,14 @@
    1.14        (BEGIN, None, None),
    1.15        (IMPORTS, None, None),
    1.16        (KEYWORDS, None, None),
    1.17 -      (HEADER, Some(((Keyword.HEADING, Nil), Nil)), None),
    1.18 -      (CHAPTER, Some(((Keyword.HEADING, Nil), Nil)), None),
    1.19 -      (SECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
    1.20 -      (SUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
    1.21 -      (SUBSUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
    1.22 +      (HEADER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.23 +      (CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.24 +      (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.25 +      (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.26 +      (SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.27 +      (TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    1.28 +      (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    1.29 +      (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
    1.30        (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
    1.31        ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
    1.32  
    1.33 @@ -110,7 +116,10 @@
    1.34          command(CHAPTER) |
    1.35          command(SECTION) |
    1.36          command(SUBSECTION) |
    1.37 -        command(SUBSUBSECTION)) ~
    1.38 +        command(SUBSUBSECTION) |
    1.39 +        command(TEXT) |
    1.40 +        command(TXT) |
    1.41 +        command(TEXT_RAW)) ~
    1.42        tags ~! document_source
    1.43  
    1.44      (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }