--- a/src/Pure/Isar/keyword.scala Tue Apr 04 22:53:01 2017 +0200
+++ b/src/Pure/Isar/keyword.scala Tue Apr 04 22:56:28 2017 +0200
@@ -93,11 +93,14 @@
/** keyword tables **/
- type Spec = ((String, List[String]), List[String])
-
- val no_spec: Spec = (("", Nil), Nil)
- val before_command_spec: Spec = ((BEFORE_COMMAND, Nil), Nil)
- val quasi_command_spec: Spec = ((QUASI_COMMAND, Nil), Nil)
+ object Spec
+ {
+ val none: Spec = Spec("")
+ }
+ sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
+ {
+ def is_none: Boolean = kind == ""
+ }
object Keywords
{
@@ -165,9 +168,13 @@
def add_keywords(header: Thy_Header.Keywords): Keywords =
(this /: header) {
- case (keywords, (name, ((kind, exts), _))) =>
- if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
- else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
+ case (keywords, (name, spec)) =>
+ if (spec.is_none)
+ keywords + Symbol.decode(name) + Symbol.encode(name)
+ else
+ keywords +
+ (Symbol.decode(name), spec.kind, spec.exts) +
+ (Symbol.encode(name), spec.kind, spec.exts)
}
--- a/src/Pure/PIDE/protocol.scala Tue Apr 04 22:53:01 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Apr 04 22:56:28 2017 +0200
@@ -361,10 +361,12 @@
val master_dir = File.standard_url(name.master_dir)
val theory = Long_Name.base_name(name.theory)
val imports = header.imports.map({ case (a, _) => a.node })
+ val keywords =
+ header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
(Nil,
pair(string, pair(string, pair(list(string), pair(list(pair(string,
pair(pair(string, list(string)), list(string)))), list(string)))))(
- (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
+ (master_dir, (theory, (imports, (keywords, header.errors)))))) },
{ case Document.Node.Perspective(a, b, c) =>
(bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
list(pair(id, pair(string, list(string))))(c.dest)) }))
--- a/src/Pure/Thy/thy_header.scala Tue Apr 04 22:53:01 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala Tue Apr 04 22:56:28 2017 +0200
@@ -39,28 +39,28 @@
val bootstrap_header: Keywords =
List(
- ("%", Keyword.no_spec),
- ("(", Keyword.no_spec),
- (")", Keyword.no_spec),
- (",", Keyword.no_spec),
- ("::", Keyword.no_spec),
- ("=", Keyword.no_spec),
- (AND, Keyword.no_spec),
- (BEGIN, Keyword.quasi_command_spec),
- (IMPORTS, Keyword.quasi_command_spec),
- (KEYWORDS, Keyword.quasi_command_spec),
- (ABBREVS, Keyword.quasi_command_spec),
- (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
- (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
- (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil))),
- (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory"))),
- ("ML", ((Keyword.THY_DECL, Nil), List("ML"))))
+ ("%", Keyword.Spec.none),
+ ("(", Keyword.Spec.none),
+ (")", Keyword.Spec.none),
+ (",", Keyword.Spec.none),
+ ("::", Keyword.Spec.none),
+ ("=", Keyword.Spec.none),
+ (AND, Keyword.Spec.none),
+ (BEGIN, Keyword.Spec(Keyword.QUASI_COMMAND)),
+ (IMPORTS, Keyword.Spec(Keyword.QUASI_COMMAND)),
+ (KEYWORDS, Keyword.Spec(Keyword.QUASI_COMMAND)),
+ (ABBREVS, Keyword.Spec(Keyword.QUASI_COMMAND)),
+ (CHAPTER, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (SECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (SUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (SUBSUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (PARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (SUBPARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (TEXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
+ (TXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
+ (TEXT_RAW, Keyword.Spec(Keyword.DOCUMENT_RAW)),
+ (THEORY, Keyword.Spec(Keyword.THY_BEGIN, tags = List("theory"))),
+ ("ML", Keyword.Spec(Keyword.THY_DECL, tags = List("ML"))))
private val bootstrap_keywords =
Keyword.Keywords.empty.add_keywords(bootstrap_header)
@@ -114,12 +114,12 @@
val keyword_spec =
atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
- { case x ~ y ~ z => ((x, y), z) }
+ { case x ~ y ~ z => Keyword.Spec(x, y, z) }
val keyword_decl =
rep1(string) ~
opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
- { case xs ~ y => xs.map((_, y.getOrElse(Keyword.no_spec))) }
+ { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) }
val keyword_decls =
keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
@@ -192,7 +192,8 @@
val f = Symbol.decode _
Thy_Header((f(name._1), name._2),
imports.map({ case (a, b) => (f(a), b) }),
- keywords.map({ case (a, ((b, c), d)) => (f(a), ((f(b), c.map(f)), d.map(f))) }),
+ keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
+ (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
abbrevs.map({ case (a, b) => (f(a), f(b)) }))
}
}