diff -r e4f363e16bdc -r 81370dfadb1d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Apr 26 13:07:20 2014 +0200
@@ -115,7 +115,7 @@
       Results.merge(states.map(_.results))
 
     def merge_markup(states: List[State], index: Markup_Index,
-        range: Text.Range, elements: Document.Elements): Markup_Tree =
+        range: Text.Range, elements: Markup.Elements): Markup_Tree =
       Markup_Tree.merge(states.map(_.markup(index)), range, elements)
   }