# HG changeset patch
# User wenzelm
# Date 1699440818 -3600
# Node ID ff4496b25197b9a0c542e338f2263d609ccf937b
# Parent  81dab48582c6bc8f4612a47a1bcca2e2f174acc0
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;

diff -r 81dab48582c6 -r ff4496b25197 src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Tue Nov 07 15:59:02 2023 +0100
+++ b/src/Pure/Isar/document_structure.scala	Wed Nov 08 11:53:38 2023 +0100
@@ -20,15 +20,14 @@
   }
   case class Atom(length: Int) extends Document
 
-  def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
-    command.span.is_kind(keywords,
-      kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
+  def is_theory_command(command: Command): Boolean =
+    command.span.is_keyword_kind(kind => Keyword.theory(kind) && !Keyword.theory_end(kind))
 
-  def is_document_command(keywords: Keyword.Keywords, command: Command): Boolean =
-    command.span.is_kind(keywords, Keyword.document, false)
+  def is_document_command(command: Command): Boolean =
+    command.span.is_keyword_kind(Keyword.document)
 
-  def is_diag_command(keywords: Keyword.Keywords, command: Command): Boolean =
-    command.span.is_kind(keywords, Keyword.diag, false)
+  def is_diag_command(command: Command): Boolean =
+    command.span.is_keyword_kind(Keyword.diag)
 
   def is_heading_command(command: Command): Boolean =
     proper_heading_level(command).isDefined
@@ -44,9 +43,8 @@
       case _ => None
     }
 
-  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
-    proper_heading_level(command) orElse
-      (if (is_theory_command(keywords, command)) Some(6) else None)
+  def heading_level(command: Command): Option[Int] =
+    proper_heading_level(command) orElse (if (is_theory_command(command)) Some(6) else None)
 
 
 
@@ -58,8 +56,7 @@
     text: CharSequence
   ): List[Document] = {
     def is_plain_theory(command: Command): Boolean =
-      is_theory_command(syntax.keywords, command) &&
-      !command.span.is_begin && !command.span.is_end
+      is_theory_command(command) && !command.span.is_begin && !command.span.is_end
 
 
     /* stack operations */
@@ -115,7 +112,7 @@
 
   object No_Item extends Item
 
-  class Sections(keywords: Keyword.Keywords) {
+  class Sections {
     private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
 
     private var stack: List[(Int, Item, mutable.ListBuffer[Document])] =
@@ -150,10 +147,10 @@
 
   /* outer syntax sections */
 
-  private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item {
+  private class Command_Item(command: Command) extends Item {
     override def name: String = command.span.name
     override def source: String = command.source
-    override def heading_level: Option[Int] = Document_Structure.heading_level(keywords, command)
+    override def heading_level: Option[Int] = Document_Structure.heading_level(command)
   }
 
   def parse_sections(
@@ -161,12 +158,11 @@
     node_name: Document.Node.Name,
     text: CharSequence
   ): List[Document] = {
-    val sections = new Sections(syntax.keywords)
+    val sections = new Sections
 
     for { span <- syntax.parse_spans(text) } {
       sections.add(
-        new Command_Item(syntax.keywords,
-          Command(Document_ID.none, node_name, Command.Blobs_Info.empty, span)))
+        new Command_Item(Command(Document_ID.none, node_name, Command.Blobs_Info.empty, span)))
     }
     sections.result()
   }
@@ -180,7 +176,7 @@
   }
 
   def parse_ml_sections(SML: Boolean, text: CharSequence): List[Document] = {
-    val sections = new Sections(Keyword.Keywords.empty)
+    val sections = new Sections
     val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None)
 
     var context: Scan.Line_Context = Scan.Finished
diff -r 81dab48582c6 -r ff4496b25197 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Nov 07 15:59:02 2023 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 08 11:53:38 2023 +0100
@@ -170,13 +170,14 @@
             case None => Command_Span.Malformed_Span
             case Some(cmd) =>
               val name = cmd.source
+              val keyword_kind = keywords.kinds.get(name)
               val offset =
                 content.takeWhile(_ != cmd).foldLeft(0) {
                   case (i, tok) => i + Symbol.length(tok.source)
                 }
               val end_offset = offset + Symbol.length(name)
               val range = Text.Range(offset, end_offset) + 1
-              Command_Span.Command_Span(name, Position.Range(range))
+              Command_Span.Command_Span(keyword_kind, name, Position.Range(range))
           }
       result += Command_Span.Span(kind, content)
     }
diff -r 81dab48582c6 -r ff4496b25197 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Tue Nov 07 15:59:02 2023 +0100
+++ b/src/Pure/PIDE/command_span.scala	Wed Nov 08 11:53:38 2023 +0100
@@ -55,15 +55,18 @@
   /* span kind */
 
   sealed abstract class Kind {
+    def keyword_kind: Option[String] = None
+
     override def toString: String =
       this match {
-        case Command_Span(name, _) => proper_string(name) getOrElse "<command>"
+        case command: Command_Span => proper_string(command.name) getOrElse "<command>"
         case Ignored_Span => "<ignored>"
         case Malformed_Span => "<malformed>"
         case Theory_Span => "<theory>"
       }
   }
-  case class Command_Span(name: String, pos: Position.T) extends Kind
+  case class Command_Span(override val keyword_kind: Option[String], name: String, pos: Position.T)
+    extends Kind
   case object Ignored_Span extends Kind
   case object Malformed_Span extends Kind
   case object Theory_Span extends Kind
@@ -87,8 +90,8 @@
         case _ => start
       }
 
-    def is_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean =
-      keywords.kinds.get(name) match {
+    def is_keyword_kind(pred: String => Boolean, other: Boolean = false): Boolean =
+      kind.keyword_kind match {
         case Some(k) => pred(k)
         case None => other
       }
diff -r 81dab48582c6 -r ff4496b25197 src/Pure/Thy/thy_element.scala
--- a/src/Pure/Thy/thy_element.scala	Tue Nov 07 15:59:02 2023 +0100
+++ b/src/Pure/Thy/thy_element.scala	Wed Nov 08 11:53:38 2023 +0100
@@ -50,7 +50,7 @@
 
   type Element_Command = Element[Command]
 
-  def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element_Command] = {
+  def parse_elements(commands: List[Command]): List[Element_Command] = {
     case class Reader(in: List[Command]) extends input.Reader[Command] {
       def first: Command = in.head
       def rest: Reader = Reader(in.tail)
@@ -73,16 +73,16 @@
           }
         }
 
-      def category(pred: String => Boolean, other: Boolean): Parser[Command] =
-        command(_.span.is_kind(keywords, pred, other))
+      def category(pred: String => Boolean, other: Boolean = false): Parser[Command] =
+        command(_.span.is_keyword_kind(pred, other = other))
 
       def theory_element: Parser[Element_Command] =
-        category(Keyword.theory_goal, false) ~ proof ^^ { case a ~ b => element(a, b) }
+        category(Keyword.theory_goal) ~ proof ^^ { case a ~ b => element(a, b) }
       def proof_element: Parser[Element_Command] =
-        category(Keyword.proof_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } |
-        category(Keyword.proof_body, true) ^^ { case a => atom(a) }
+        category(Keyword.proof_goal) ~ proof ^^ { case a ~ b => element(a, b) } |
+        category(Keyword.proof_body, other = true) ^^ { case a => atom(a) }
       def proof: Parser[Proof[Command]] =
-        rep(proof_element) ~ category(Keyword.qed, false) ^^ { case a ~ b => (a, b) }
+        rep(proof_element) ~ category(Keyword.qed) ^^ { case a ~ b => (a, b) }
 
       val default_element: Parser[Element_Command] = command(_ => true) ^^ { case a => atom(a) }