src/Pure/PIDE/command.scala

 
   sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)
 
   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)(_ ++ _)
   }
 
   final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
   {

       rep.getOrElse(index, Markup_Tree.empty)
 
     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))))
     }