src/Pure/Thy/thy_header.scala
changeset 65384 36255c43c64c
parent 65362 908a27a4b9c9
child 65392 f365f61f2081
     1.1 --- a/src/Pure/Thy/thy_header.scala	Tue Apr 04 22:53:01 2017 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Apr 04 22:56:28 2017 +0200
     1.3 @@ -39,28 +39,28 @@
     1.4  
     1.5    val bootstrap_header: Keywords =
     1.6      List(
     1.7 -      ("%", Keyword.no_spec),
     1.8 -      ("(", Keyword.no_spec),
     1.9 -      (")", Keyword.no_spec),
    1.10 -      (",", Keyword.no_spec),
    1.11 -      ("::", Keyword.no_spec),
    1.12 -      ("=", Keyword.no_spec),
    1.13 -      (AND, Keyword.no_spec),
    1.14 -      (BEGIN, Keyword.quasi_command_spec),
    1.15 -      (IMPORTS, Keyword.quasi_command_spec),
    1.16 -      (KEYWORDS, Keyword.quasi_command_spec),
    1.17 -      (ABBREVS, Keyword.quasi_command_spec),
    1.18 -      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    1.19 -      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    1.20 -      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    1.21 -      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    1.22 -      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    1.23 -      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    1.24 -      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
    1.25 -      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
    1.26 -      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil))),
    1.27 -      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory"))),
    1.28 -      ("ML", ((Keyword.THY_DECL, Nil), List("ML"))))
    1.29 +      ("%", Keyword.Spec.none),
    1.30 +      ("(", Keyword.Spec.none),
    1.31 +      (")", Keyword.Spec.none),
    1.32 +      (",", Keyword.Spec.none),
    1.33 +      ("::", Keyword.Spec.none),
    1.34 +      ("=", Keyword.Spec.none),
    1.35 +      (AND, Keyword.Spec.none),
    1.36 +      (BEGIN, Keyword.Spec(Keyword.QUASI_COMMAND)),
    1.37 +      (IMPORTS, Keyword.Spec(Keyword.QUASI_COMMAND)),
    1.38 +      (KEYWORDS, Keyword.Spec(Keyword.QUASI_COMMAND)),
    1.39 +      (ABBREVS, Keyword.Spec(Keyword.QUASI_COMMAND)),
    1.40 +      (CHAPTER, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    1.41 +      (SECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    1.42 +      (SUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    1.43 +      (SUBSUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    1.44 +      (PARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    1.45 +      (SUBPARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    1.46 +      (TEXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
    1.47 +      (TXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
    1.48 +      (TEXT_RAW, Keyword.Spec(Keyword.DOCUMENT_RAW)),
    1.49 +      (THEORY, Keyword.Spec(Keyword.THY_BEGIN, tags = List("theory"))),
    1.50 +      ("ML", Keyword.Spec(Keyword.THY_DECL, tags = List("ML"))))
    1.51  
    1.52    private val bootstrap_keywords =
    1.53      Keyword.Keywords.empty.add_keywords(bootstrap_header)
    1.54 @@ -114,12 +114,12 @@
    1.55  
    1.56      val keyword_spec =
    1.57        atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    1.58 -      { case x ~ y ~ z => ((x, y), z) }
    1.59 +      { case x ~ y ~ z => Keyword.Spec(x, y, z) }
    1.60  
    1.61      val keyword_decl =
    1.62        rep1(string) ~
    1.63        opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
    1.64 -      { case xs ~ y => xs.map((_, y.getOrElse(Keyword.no_spec))) }
    1.65 +      { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) }
    1.66  
    1.67      val keyword_decls =
    1.68        keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    1.69 @@ -192,7 +192,8 @@
    1.70      val f = Symbol.decode _
    1.71      Thy_Header((f(name._1), name._2),
    1.72        imports.map({ case (a, b) => (f(a), b) }),
    1.73 -      keywords.map({ case (a, ((b, c), d)) => (f(a), ((f(b), c.map(f)), d.map(f))) }),
    1.74 +      keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
    1.75 +        (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
    1.76        abbrevs.map({ case (a, b) => (f(a), f(b)) }))
    1.77    }
    1.78  }