# 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)) }))
 }