# HG changeset patch # User wenzelm # Date 1308311753 -7200 # Node ID 6ed49c52d4635e2e41a92e0dc616dd57a58d8ae7 # Parent c69e9fbb81a85357147ea78dd644d9cde61c911b flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec); diff -r c69e9fbb81a8 -r 6ed49c52d463 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Fri Jun 17 00:10:39 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Fri Jun 17 13:55:53 2011 +0200 @@ -69,7 +69,7 @@ private val session = model.session - /** robust extension body **/ + /* robust extension body */ def robust_body[A](default: A)(body: => A): A = { @@ -85,8 +85,6 @@ } - /** token handling **/ - /* visible line ranges */ // simplify slightly odd result of TextArea.getScreenLineEndOffset etc. @@ -112,6 +110,31 @@ } + /* snapshot */ + + // owned by Swing thread + @volatile private var was_outdated = false + @volatile private var was_updated = false + + def update_snapshot(): Document.Snapshot = + { + Swing_Thread.require() + val snapshot = model.snapshot() + was_updated = was_outdated && !snapshot.is_outdated + was_outdated = was_outdated || snapshot.is_outdated + snapshot + } + + def flush_snapshot(): (Boolean, Document.Snapshot) = + { + Swing_Thread.require() + val snapshot = update_snapshot() + val updated = was_updated + if (updated) { was_outdated = false; was_updated = false } + (updated, snapshot) + } + + /* HTML popups */ private var html_popup: Option[Popup] = None @@ -196,7 +219,7 @@ if (!model.buffer.isLoaded) exit_control() else Isabelle.swing_buffer_lock(model.buffer) { - val snapshot = model.snapshot + val snapshot = update_snapshot() if (control) init_popup(snapshot, x, y) @@ -217,7 +240,7 @@ override def getToolTipText(x: Int, y: Int): String = { robust_body(null: String) { - val snapshot = model.snapshot() + val snapshot = update_snapshot() val offset = text_area.xyToOffset(x, y) if (control) { snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match @@ -249,14 +272,14 @@ val width = GutterOptionPane.getSelectionAreaWidth val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3) val FOLD_MARKER_SIZE = 12 - + if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) { Isabelle.swing_buffer_lock(model.buffer) { - val snapshot = model.snapshot() + val snapshot = update_snapshot() for (i <- 0 until physical_lines.length) { if (physical_lines(i) != -1) { val line_range = proper_line_range(start(i), end(i)) - + // gutter icons val icons = (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate @@ -284,7 +307,7 @@ def selected_command(): Option[Command] = { Swing_Thread.require() - model.snapshot().node.proper_command_at(text_area.getCaretPosition) + update_snapshot().node.proper_command_at(text_area.getCaretPosition) } private val caret_listener = new CaretListener { @@ -331,7 +354,7 @@ val buffer = model.buffer Isabelle.buffer_lock(buffer) { - val snapshot = model.snapshot() + val snapshot = update_snapshot() def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] = { @@ -372,22 +395,26 @@ case Session.Commands_Changed(changed) => val buffer = model.buffer Isabelle.swing_buffer_lock(buffer) { - val snapshot = model.snapshot() + val (updated, snapshot) = flush_snapshot() + val visible_range = screen_lines_range() - if (changed.exists(snapshot.node.commands.contains)) + if (updated || changed.exists(snapshot.node.commands.contains)) overview.repaint() - val visible_range = screen_lines_range() - val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1) - if (visible_cmds.exists(changed)) { - for { - line <- 0 until text_area.getVisibleLines - val start = text_area.getScreenLineStartOffset(line) if start >= 0 - val end = text_area.getScreenLineEndOffset(line) if end >= 0 - val range = proper_line_range(start, end) - val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) - if line_cmds.exists(changed) - } text_area.invalidateScreenLineRange(line, line) + if (updated) invalidate_line_range(visible_range) + else { + val visible_cmds = + snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1) + if (visible_cmds.exists(changed)) { + for { + line <- 0 until text_area.getVisibleLines + val start = text_area.getScreenLineStartOffset(line) if start >= 0 + val end = text_area.getScreenLineEndOffset(line) if end >= 0 + val range = proper_line_range(start, end) + val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) + if line_cmds.exists(changed) + } text_area.invalidateScreenLineRange(line, line) + } } } diff -r c69e9fbb81a8 -r 6ed49c52d463 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Fri Jun 17 00:10:39 2011 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Fri Jun 17 13:55:53 2011 +0200 @@ -34,7 +34,7 @@ Document_View(view.getTextArea) match { case Some(doc_view) => val cmd = current_command.get - val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get + val start_ofs = doc_view.update_snapshot().node.command_start(cmd).get val buffer = view.getBuffer buffer.beginCompoundEdit() buffer.remove(start_ofs, cmd.length) @@ -83,7 +83,7 @@ case Some(doc_view) => current_command match { case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => - val snapshot = doc_view.model.snapshot() + val snapshot = doc_view.update_snapshot() val filtered_results = snapshot.state(cmd).results.iterator.map(_._2) filter { case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable diff -r c69e9fbb81a8 -r 6ed49c52d463 src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Fri Jun 17 00:10:39 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Fri Jun 17 13:55:53 2011 +0200 @@ -53,7 +53,7 @@ start: Array[Int], end: Array[Int], y: Int, line_height: Int) { doc_view.robust_body(()) { - painter_snapshot = model.snapshot() + painter_snapshot = doc_view.update_snapshot() painter_clip = gfx.getClip } }