--- a/src/Pure/PIDE/markup.ML Wed Nov 03 16:19:49 2021 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Nov 03 16:23:20 2021 +0100
@@ -158,6 +158,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 commandN: string val command_properties: T -> T
val keywordN: string val keyword_properties: T -> T
val stringN: string val string: T
@@ -592,6 +593,7 @@
(* outer syntax *)
val (command_keywordN, command_keyword) = markup_elem "command_keyword";
+val (command_spanN, command_span) = markup_string "command_span" nameN;
val commandN = "command"; val command_properties = properties [(kindN, commandN)];
val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];