diff -r 9dda93a753b1 -r d5d0e36eda16 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Dec 07 20:26:09 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Dec 07 21:49:39 2020 +0100
@@ -131,8 +131,10 @@
 
   object Markups
   {
+    type Entry = (Markup_Index, Markup_Tree)
     val empty: Markups = new Markups(Map.empty)
     def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
+    def make(args: TraversableOnce[Entry]): Markups = (empty /: args)(_ + _)
     def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
   }
 
@@ -146,7 +148,7 @@
     def add(index: Markup_Index, markup: Text.Markup): Markups =
       new Markups(rep + (index -> (this(index) + markup)))
 
-    def + (entry: (Markup_Index, Markup_Tree)): Markups =
+    def + (entry: Markups.Entry): Markups =
     {
       val (index, tree) = entry
       new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full))))