src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Mon Jun 30 11:28:04 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Jun 30 12:42:21 2025 +0200
@@ -133,6 +133,8 @@
     def apply(index: Markup_Index): Markup_Tree =
       rep.getOrElse(index, Markup_Tree.empty)
 
+    def add(markup: Text.Markup): Markups = add(Markup_Index.markup, markup)
+
     def add(index: Markup_Index, markup: Text.Markup): Markups =
       new Markups(rep + (index -> (this(index) + markup)))