author | wenzelm |
Mon, 09 Jan 2012 23:09:03 +0100 | |
changeset 46165 | 0e131ca93a49 |
parent 46164 | a01c969f2e14 |
child 46166 | 4beb2f41ed93 |
--- 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 })