--- a/src/Pure/PIDE/markup.scala Tue Jul 29 16:43:49 2025 +0200
+++ b/src/Pure/PIDE/markup.scala Tue Jul 29 17:01:57 2025 +0200
@@ -464,6 +464,8 @@
else None
}
+ val COMMAND_RANGE = "command_range"
+
val COMMAND = "command"
val KEYWORD = "keyword"
val KEYWORD1 = "keyword1"