--- a/src/Tools/jEdit/src/text_overview.scala Sat Mar 23 13:57:46 2013 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Sat Mar 23 16:10:46 2013 +0100
@@ -101,7 +101,7 @@
if (!(line_count == last_line_count && char_count == last_char_count &&
L == last_L && H == last_H && relevant_range == last_relevant_range &&
- (snapshot eq_markup last_snapshot) && (options eq last_options)))
+ (snapshot eq_content last_snapshot) && (options eq last_options)))
{
@tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
: List[(Color, Int, Int)] =