src/Pure/Thy/thy_header.scala
changeset 63429 baedd4724f08
parent 63022 785a59235a15
child 63448 998acd66fbd7
     1.1 --- a/src/Pure/Thy/thy_header.scala	Fri Jul 08 22:22:51 2016 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 11:18:35 2016 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  {
     1.5    /* bootstrap keywords */
     1.6  
     1.7 -  type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
     1.8 +  type Keywords = List[(String, Keyword.Spec, Option[String])]
     1.9  
    1.10    val CHAPTER = "chapter"
    1.11    val SECTION = "section"
    1.12 @@ -37,27 +37,27 @@
    1.13  
    1.14    private val bootstrap_header: Keywords =
    1.15      List(
    1.16 -      ("%", None, None),
    1.17 -      ("(", None, None),
    1.18 -      (")", None, None),
    1.19 -      (",", None, None),
    1.20 -      ("::", None, None),
    1.21 -      ("==", None, None),
    1.22 -      (AND, None, None),
    1.23 -      (BEGIN, None, None),
    1.24 -      (IMPORTS, None, None),
    1.25 -      (KEYWORDS, None, None),
    1.26 -      (CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.27 -      (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.28 -      (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.29 -      (SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.30 -      (PARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.31 -      (SUBPARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.32 -      (TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    1.33 -      (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    1.34 -      (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
    1.35 -      (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
    1.36 -      ("ML", Some((Keyword.THY_DECL, Nil), List("ML")), None))
    1.37 +      ("%", Keyword.no_spec, None),
    1.38 +      ("(", Keyword.no_spec, None),
    1.39 +      (")", Keyword.no_spec, None),
    1.40 +      (",", Keyword.no_spec, None),
    1.41 +      ("::", Keyword.no_spec, None),
    1.42 +      ("==", Keyword.no_spec, None),
    1.43 +      (AND, Keyword.no_spec, None),
    1.44 +      (BEGIN, Keyword.no_spec, None),
    1.45 +      (IMPORTS, Keyword.no_spec, None),
    1.46 +      (KEYWORDS, Keyword.no_spec, None),
    1.47 +      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.48 +      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.49 +      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.50 +      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.51 +      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.52 +      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    1.53 +      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    1.54 +      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    1.55 +      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
    1.56 +      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory")), None),
    1.57 +      ("ML", ((Keyword.THY_DECL, Nil), List("ML")), None))
    1.58  
    1.59    private val bootstrap_keywords =
    1.60      Keyword.Keywords.empty.add_keywords(bootstrap_header)
    1.61 @@ -108,7 +108,7 @@
    1.62        rep1(string) ~
    1.63        opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    1.64        opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
    1.65 -      { case xs ~ y ~ z => xs.map((_, y, z)) }
    1.66 +      { case xs ~ y ~ z => xs.map((_, y.getOrElse(Keyword.no_spec), z)) }
    1.67  
    1.68      val keyword_decls =
    1.69        keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    1.70 @@ -177,7 +177,7 @@
    1.71    {
    1.72      val f = Symbol.decode _
    1.73      Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
    1.74 -      keywords.map({ case (a, b, c) =>
    1.75 -        (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
    1.76 +      keywords.map({ case (a, ((x, y), z), c) =>
    1.77 +        (f(a), ((f(x), y.map(f)), z.map(f)), c.map(f)) }))
    1.78    }
    1.79  }