83 Log.log(Log.ERROR, this, ERROR("Inconsistent document model")) |
83 Log.log(Log.ERROR, this, ERROR("Inconsistent document model")) |
84 default |
84 default |
85 } |
85 } |
86 } |
86 } |
87 catch { case t: Throwable => Log.log(Log.ERROR, this, t); default } |
87 catch { case t: Throwable => Log.log(Log.ERROR, this, t); default } |
88 } |
|
89 |
|
90 |
|
91 /* visible text range */ |
|
92 |
|
93 // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength |
|
94 def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range = |
|
95 Text.Range(start, end min model.buffer.getLength) |
|
96 |
|
97 def visible_range(): Option[Text.Range] = |
|
98 { |
|
99 val n = text_area.getVisibleLines |
|
100 if (n > 0) { |
|
101 val start = text_area.getScreenLineStartOffset(0) |
|
102 val raw_end = text_area.getScreenLineEndOffset(n - 1) |
|
103 Some(proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)) |
|
104 } |
|
105 else None |
|
106 } |
|
107 |
|
108 def invalidate_range(range: Text.Range) |
|
109 { |
|
110 text_area.invalidateLineRange( |
|
111 model.buffer.getLineOfOffset(range.start), |
|
112 model.buffer.getLineOfOffset(range.stop)) |
|
113 } |
88 } |
114 |
89 |
115 |
90 |
116 /* perspective */ |
91 /* perspective */ |
117 |
92 |
154 def update(new_info: Option[Text.Info[A]]) |
129 def update(new_info: Option[Text.Info[A]]) |
155 { |
130 { |
156 val old_info = the_info |
131 val old_info = the_info |
157 if (new_info != old_info) { |
132 if (new_info != old_info) { |
158 for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt } |
133 for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt } |
159 invalidate_range(range) |
134 JEdit_Lib.invalidate_range(text_area, range) |
160 the_info = new_info |
135 the_info = new_info |
161 } |
136 } |
162 } |
137 } |
163 |
138 |
164 def update_rendering(r: Isabelle_Rendering, range: Text.Range) |
139 def update_rendering(r: Isabelle_Rendering, range: Text.Range) |
247 val width = GutterOptionPane.getSelectionAreaWidth |
222 val width = GutterOptionPane.getSelectionAreaWidth |
248 val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3) |
223 val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3) |
249 val FOLD_MARKER_SIZE = 12 |
224 val FOLD_MARKER_SIZE = 12 |
250 |
225 |
251 if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) { |
226 if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) { |
252 JEdit_Lib.buffer_lock(model.buffer) { |
227 val buffer = model.buffer |
|
228 JEdit_Lib.buffer_lock(buffer) { |
253 val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value) |
229 val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value) |
254 |
230 |
255 for (i <- 0 until physical_lines.length) { |
231 for (i <- 0 until physical_lines.length) { |
256 if (physical_lines(i) != -1) { |
232 if (physical_lines(i) != -1) { |
257 val line_range = proper_line_range(start(i), end(i)) |
233 val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i)) |
258 |
234 |
259 // gutter icons |
235 // gutter icons |
260 rendering.gutter_message(line_range) match { |
236 rendering.gutter_message(line_range) match { |
261 case Some(icon) => |
237 case Some(icon) => |
262 val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10 |
238 val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10 |
316 if (changed.assignment || |
292 if (changed.assignment || |
317 (changed.nodes.contains(model.name) && |
293 (changed.nodes.contains(model.name) && |
318 changed.commands.exists(snapshot.node.commands.contains))) |
294 changed.commands.exists(snapshot.node.commands.contains))) |
319 Swing_Thread.later { overview.delay_repaint.invoke() } |
295 Swing_Thread.later { overview.delay_repaint.invoke() } |
320 |
296 |
321 visible_range() match { |
297 JEdit_Lib.visible_range(text_area) match { |
322 case Some(visible) => |
298 case Some(visible) => |
323 if (changed.assignment) invalidate_range(visible) |
299 if (changed.assignment) JEdit_Lib.invalidate_range(text_area, visible) |
324 else { |
300 else { |
325 val visible_cmds = |
301 val visible_cmds = |
326 snapshot.node.command_range(snapshot.revert(visible)).map(_._1) |
302 snapshot.node.command_range(snapshot.revert(visible)).map(_._1) |
327 if (visible_cmds.exists(changed.commands)) { |
303 if (visible_cmds.exists(changed.commands)) { |
328 for { |
304 for { |
329 line <- 0 until text_area.getVisibleLines |
305 line <- 0 until text_area.getVisibleLines |
330 start = text_area.getScreenLineStartOffset(line) if start >= 0 |
306 start = text_area.getScreenLineStartOffset(line) if start >= 0 |
331 end = text_area.getScreenLineEndOffset(line) if end >= 0 |
307 end = text_area.getScreenLineEndOffset(line) if end >= 0 |
332 range = proper_line_range(start, end) |
308 range = JEdit_Lib.proper_line_range(buffer, start, end) |
333 line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) |
309 line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) |
334 if line_cmds.exists(changed.commands) |
310 if line_cmds.exists(changed.commands) |
335 } text_area.invalidateScreenLineRange(line, line) |
311 } text_area.invalidateScreenLineRange(line, line) |
336 } |
312 } |
337 } |
313 } |