diff -r 5717310a0c6a -r dab089b25eb6 src/Pure/PIDE/markup.ML
--- 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)];