# HG changeset patch # User wenzelm # Date 1606598448 -3600 # Node ID 722c0d02ffabc74a689fdd987641bfedc6e5ed58 # Parent 3cc73d00553c40c786242a706c6588458838f23d clarified signature; diff -r 3cc73d00553c -r 722c0d02ffab src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Sat Nov 28 21:56:24 2020 +0100 +++ b/src/Pure/Isar/keyword.scala Sat Nov 28 22:20:48 2020 +0100 @@ -106,18 +106,18 @@ /** keyword tables **/ - object Spec + sealed case class Spec( + kind: String = "", + load_command: String = "", + tags: List[String] = Nil) { - val none: Spec = Spec("") - } - sealed case class Spec(kind: String, load_command: String = "", tags: List[String] = Nil) - { - def is_none: Boolean = kind == "" - override def toString: String = kind + (if (load_command.isEmpty) "" else " (" + quote(load_command) + ")") + (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", "")) + + def map(f: String => String): Spec = + copy(kind = f(kind), load_command = f(load_command), tags = tags.map(f)) } object Keywords @@ -187,7 +187,7 @@ def add_keywords(header: Thy_Header.Keywords): Keywords = (this /: header) { case (keywords, (name, spec)) => - if (spec.is_none) + if (spec.kind.isEmpty) keywords + Symbol.decode(name) + Symbol.encode(name) else keywords + diff -r 3cc73d00553c -r 722c0d02ffab src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sat Nov 28 21:56:24 2020 +0100 +++ b/src/Pure/PIDE/protocol.scala Sat Nov 28 22:20:48 2020 +0100 @@ -398,7 +398,7 @@ { case Document.Node.Deps(header) => val master_dir = File.standard_url(name.master_dir) val imports = header.imports.map(_.node) - val keywords = header.keywords.map({ case (a, Keyword.Spec(b, _, c)) => (a, (b, c)) }) + val keywords = header.keywords.map({ case (a, spec) => (a, (spec.kind, spec.tags)) }) (Nil, pair(string, pair(string, pair(list(string), pair(list(pair(string, pair(string, list(string)))), list(string)))))( diff -r 3cc73d00553c -r 722c0d02ffab src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sat Nov 28 21:56:24 2020 +0100 +++ b/src/Pure/Thy/thy_header.scala Sat Nov 28 22:20:48 2020 +0100 @@ -37,28 +37,28 @@ val bootstrap_header: Keywords = List( - ("%", 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")))) + ("%", Keyword.Spec()), + ("(", Keyword.Spec()), + (")", Keyword.Spec()), + (",", Keyword.Spec()), + ("::", Keyword.Spec()), + ("=", Keyword.Spec()), + (AND, Keyword.Spec()), + (BEGIN, Keyword.Spec(kind = Keyword.QUASI_COMMAND)), + (IMPORTS, Keyword.Spec(kind = Keyword.QUASI_COMMAND)), + (KEYWORDS, Keyword.Spec(kind = Keyword.QUASI_COMMAND)), + (ABBREVS, Keyword.Spec(kind = Keyword.QUASI_COMMAND)), + (CHAPTER, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), + (SECTION, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), + (SUBSECTION, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), + (SUBSUBSECTION, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), + (PARAGRAPH, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), + (SUBPARAGRAPH, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), + (TEXT, Keyword.Spec(kind = Keyword.DOCUMENT_BODY)), + (TXT, Keyword.Spec(kind = Keyword.DOCUMENT_BODY)), + (TEXT_RAW, Keyword.Spec(kind = Keyword.DOCUMENT_RAW)), + (THEORY, Keyword.Spec(kind = Keyword.THY_BEGIN, tags = List("theory"))), + ("ML", Keyword.Spec(kind = Keyword.THY_DECL, tags = List("ML")))) private val bootstrap_keywords = Keyword.Keywords.empty.add_keywords(bootstrap_header) @@ -137,12 +137,12 @@ val keyword_spec = (atom("outer syntax keyword specification", _.is_name) >> load_command_spec) ~ tags ^^ - { case (x, y) ~ z => Keyword.Spec(x, y, z) } + { case (x, y) ~ z => Keyword.Spec(kind = x, load_command = y, tags = z) } val keyword_decl = rep1(string) ~ opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^ - { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) } + { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec()))) } val keyword_decls = keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ @@ -160,15 +160,7 @@ { case None => Nil case Some(_ ~ xs) => xs }) ~ (opt($$$(ABBREVS) ~! abbrevs) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ - $$$(BEGIN) ^^ - { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ => - val f = Symbol.decode _ - Thy_Header((f(name), pos), - imports.map({ case (a, b) => (f(a), b) }), - keywords.map({ case (a, Keyword.Spec(b, c, d)) => - (f(a), Keyword.Spec(f(b), f(c), d.map(f))) }), - abbrevs.map({ case (a, b) => (f(a), f(b)) })) - } + $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a, b, c, d).map(Symbol.decode) } val heading = (command(CHAPTER) | @@ -240,4 +232,10 @@ def name: String = name_pos._1 def pos: Position.T = name_pos._2 def imports: List[String] = imports_pos.map(_._1) + + def map(f: String => String): Thy_Header = + Thy_Header((f(name), pos), + imports_pos.map({ case (a, b) => (f(a), b) }), + keywords.map({ case (a, spec) => (f(a), spec.map(f)) }), + abbrevs.map({ case (a, b) => (f(a), f(b)) })) }