more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax;

--- a/src/Pure/PIDE/command.ML	Sun Jul 09 16:29:13 2023 +0200
+++ b/src/Pure/PIDE/command.ML	Sun Jul 09 17:39:46 2023 +0200
@@ -123,7 +123,12 @@
       else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span);
     val _ =
       if Toplevel.is_ignored tr orelse Toplevel.is_malformed tr then ()
-      else Position.report (#1 core_range) (Markup.command_span (Toplevel.name_of tr));
+      else
+        let
+          val name = Toplevel.name_of tr;
+          val kind = the_default "" (Keyword.command_kind (Thy_Header.get_keywords thy) name);
+          val markup = Markup.command_span {name = name, kind = kind};
+        in Position.report (#1 core_range) markup end;
   in tr end;
 
 end;

--- a/src/Pure/PIDE/markup.ML	Sun Jul 09 16:29:13 2023 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun Jul 09 17:39:46 2023 +0200
@@ -172,7 +172,7 @@
   val descriptionN: string
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
-  val command_spanN: string val command_span: string -> T
+  val command_spanN: string val command_span: {name: string, kind: string} -> T
   val commandN: string val command_properties: T -> T
   val keywordN: string val keyword_properties: T -> T
   val stringN: string val string: T
@@ -630,7 +630,11 @@
 (* outer syntax *)
 
 val (command_keywordN, command_keyword) = markup_elem "command_keyword";
-val (command_spanN, command_span) = markup_string "command_span" nameN;
+
+val command_spanN = "command_span";
+fun command_span {name, kind} : T =
+  (command_spanN,
+    (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
 
 val commandN = "command"; val command_properties = properties [(kindN, commandN)];
 val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];

--- a/src/Pure/PIDE/markup.scala	Sun Jul 09 16:29:13 2023 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun Jul 09 17:39:46 2023 +0200
@@ -420,7 +420,22 @@
   /* outer syntax */
 
   val COMMAND_SPAN = "command_span"
-  val Command_Span = new Markup_String(COMMAND_SPAN, NAME)
+  object Command_Span {
+    sealed case class Arg(name: String, kind: String) {
+      def properties: Properties.T =
+        (if (name.isEmpty) Nil else Name(name)) :::
+        (if (kind.isEmpty) Nil else Kind(kind))
+    }
+
+    def apply(arg: Arg): Markup = Markup(COMMAND_SPAN, arg.properties)
+    def apply(name: String, kind: String): Markup = apply(Arg(name, kind))
+
+    def unapply(markup: Markup): Option[Arg] =
+      if (markup.name == COMMAND_SPAN) {
+        Some(Arg(Name.get(markup.properties), Kind.get(markup.properties)))
+      }
+      else None
+  }
 
   val COMMAND = "command"
   val KEYWORD = "keyword"