diff -r 1a8fd26fedb6 -r eae5fa0055bd src/Pure/PIDE/markup.ML
--- 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)];