# HG changeset patch
# User wenzelm
# Date 1326146943 -3600
# Node ID 0e131ca93a492248bf45f8c7cd6a4407bea937fd
# Parent  a01c969f2e143bf854e714d1c4b9f9656f172321
proper cumulation of bulk arguments;

diff -r a01c969f2e14 -r 0e131ca93a49 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Mon Jan 09 23:08:33 2012 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Mon Jan 09 23:09:03 2012 +0100
@@ -117,7 +117,7 @@
           (entry.markup :\ (x, false))((info, res) =>
             {
               val (y, changed) = res
-              val arg = (x, Text.Info(entry.range, info))
+              val arg = (y, Text.Info(entry.range, info))
               if (body.result.isDefinedAt(arg)) (body.result(arg), true)
               else res
             })