--- 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)];