# HG changeset patch
# User wenzelm
# Date 1373711985 -7200
# Node ID 84eb792224a80f3103971857cddbcf00269b6164
# Parent  c56b6fa636e8cbd2625d319dcaac64c529e124df
full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);

diff -r c56b6fa636e8 -r 84eb792224a8 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Jul 13 00:50:49 2013 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Jul 13 12:39:45 2013 +0200
@@ -130,7 +130,10 @@
       }
 
     def ++ (other: State): State =
-      copy(results = results ++ other.results)  // FIXME merge more content!?
+      copy(
+        status = other.status ::: status,
+        results = results ++ other.results,
+        markup = markup ++ other.markup)
   }
 
 
diff -r c56b6fa636e8 -r 84eb792224a8 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sat Jul 13 00:50:49 2013 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Jul 13 12:39:45 2013 +0200
@@ -184,6 +184,10 @@
     }
   }
 
+  def ++ (other: Markup_Tree): Markup_Tree =
+    (this /: other.branches)({ case (tree, (range, entry)) =>
+      ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) })
+
   def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
   {
     def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =