--- 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))))