53 |
53 |
54 private var cached_colors: List[(Color, Int, Int)] = Nil |
54 private var cached_colors: List[(Color, Int, Int)] = Nil |
55 |
55 |
56 private var last_snapshot = Document.State.init.snapshot() |
56 private var last_snapshot = Document.State.init.snapshot() |
57 private var last_options = Isabelle.options.value |
57 private var last_options = Isabelle.options.value |
|
58 private var last_relevant_range = Text.Range(0) |
58 private var last_line_count = 0 |
59 private var last_line_count = 0 |
59 private var last_char_count = 0 |
60 private var last_char_count = 0 |
60 private var last_L = 0 |
61 private var last_L = 0 |
61 private var last_H = 0 |
62 private var last_H = 0 |
62 |
63 |
65 super.paintComponent(gfx) |
66 super.paintComponent(gfx) |
66 Swing_Thread.assert() |
67 Swing_Thread.assert() |
67 |
68 |
68 doc_view.rich_text_area.robust_body(()) { |
69 doc_view.rich_text_area.robust_body(()) { |
69 JEdit_Lib.buffer_lock(buffer) { |
70 JEdit_Lib.buffer_lock(buffer) { |
70 val snapshot = doc_view.model.snapshot() |
71 val rendering = doc_view.get_rendering() |
|
72 val snapshot = rendering.snapshot |
|
73 val options = rendering.options |
71 |
74 |
72 if (snapshot.is_outdated || !Isabelle.options.bool("jedit_text_overview")) { |
75 if (snapshot.is_outdated) { |
73 gfx.setColor(Isabelle.options.color_value("outdated_color")) |
76 gfx.setColor(rendering.outdated_color) |
74 gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) |
77 gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) |
75 } |
78 } |
76 else { |
79 else { |
77 gfx.setColor(getBackground) |
80 gfx.setColor(getBackground) |
78 gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) |
81 gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) |
81 val char_count = buffer.getLength |
84 val char_count = buffer.getLength |
82 |
85 |
83 val L = lines() |
86 val L = lines() |
84 val H = getHeight() |
87 val H = getHeight() |
85 |
88 |
86 val options = Isabelle.options.value |
89 val relevant_range = |
|
90 JEdit_Lib.visible_range(text_area) match { |
|
91 case None => Text.Range(0) |
|
92 case Some(visible_range) => |
|
93 val len = rendering.overview_limit max visible_range.length |
|
94 val start = ((visible_range.start + visible_range.stop - len) / 2) max 0 |
|
95 val stop = (start + len) min char_count |
|
96 Text.Range(start, stop) |
|
97 } |
87 |
98 |
88 if (!(line_count == last_line_count && char_count == last_char_count && |
99 if (!(line_count == last_line_count && char_count == last_char_count && |
89 L == last_L && H == last_H && (snapshot eq_markup last_snapshot) && |
100 L == last_L && H == last_H && relevant_range == last_relevant_range && |
90 (options eq last_options))) |
101 (snapshot eq_markup last_snapshot) && (options eq last_options))) |
91 { |
102 { |
92 val rendering = Isabelle_Rendering(snapshot, options) |
|
93 |
|
94 @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)]) |
103 @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)]) |
95 : List[(Color, Int, Int)] = |
104 : List[(Color, Int, Int)] = |
96 { |
105 { |
97 if (l < line_count && h < H) { |
106 if (l < line_count && h < H) { |
98 val p1 = p + H |
107 val p1 = p + H |
105 val end = |
114 val end = |
106 if (l1 < line_count) buffer.getLineStartOffset(l1) |
115 if (l1 < line_count) buffer.getLineStartOffset(l1) |
107 else char_count |
116 else char_count |
108 val range = Text.Range(start, end) |
117 val range = Text.Range(start, end) |
109 |
118 |
|
119 val range_color = |
|
120 if (range overlaps relevant_range) rendering.overview_color(range) |
|
121 else Some(rendering.outdated_color) |
110 val colors1 = |
122 val colors1 = |
111 (rendering.overview_color(range), colors) match { |
123 (range_color, colors) match { |
112 case (Some(color), (old_color, old_h, old_h1) :: rest) |
124 case (Some(color), (old_color, old_h, old_h1) :: rest) |
113 if color == old_color && old_h1 == h => (color, old_h, h1) :: rest |
125 if color == old_color && old_h1 == h => (color, old_h, h1) :: rest |
114 case (Some(color), _) => (color, h, h1) :: colors |
126 case (Some(color), _) => (color, h, h1) :: colors |
115 case (None, _) => colors |
127 case (None, _) => colors |
116 } |
128 } |
120 } |
132 } |
121 cached_colors = loop(0, 0, 0, 0, Nil) |
133 cached_colors = loop(0, 0, 0, 0, Nil) |
122 |
134 |
123 last_snapshot = snapshot |
135 last_snapshot = snapshot |
124 last_options = options |
136 last_options = options |
|
137 last_relevant_range = relevant_range |
125 last_line_count = line_count |
138 last_line_count = line_count |
126 last_char_count = char_count |
139 last_char_count = char_count |
127 last_L = L |
140 last_L = L |
128 last_H = H |
141 last_H = H |
129 } |
142 } |