# HG changeset patch # User wenzelm # Date 1491339388 -7200 # Node ID 36255c43c64cc9d7ab3f22f8e66b8d1bc1fd9828 # Parent 089f2edefb77a6ec5362114fbe6fbc49ed69bd94 more explicit types; diff -r 089f2edefb77 -r 36255c43c64c src/Pure/Isar/keyword.scala --- 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) } diff -r 089f2edefb77 -r 36255c43c64c src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Tue Apr 04 22:53:01 2017 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Tue Apr 04 22:56:28 2017 +0200 @@ -71,8 +71,10 @@ def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = (this /: keywords) { - case (syntax, (name, ((kind, exts), _))) => - syntax + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts) + case (syntax, (name, spec)) => + syntax + + (Symbol.decode(name), spec.kind, spec.exts) + + (Symbol.encode(name), spec.kind, spec.exts) } diff -r 089f2edefb77 -r 36255c43c64c src/Pure/PIDE/protocol.scala --- 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)) })) diff -r 089f2edefb77 -r 36255c43c64c src/Pure/Thy/thy_header.scala --- 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)) })) } }