# HG changeset patch # User wenzelm # Date 1332194907 -3600 # Node ID fc3bb6c02a3c03e593abfc689cdc36cc805a82ac # Parent 36dacca8a95cc173a5cf1e4d9dd20bc034dc1686 explicit propagation of assignment event, even if changed command set is empty; discontinued slightly odd Document_View.update_snapshot/flush_snapshot; diff -r 36dacca8a95c -r fc3bb6c02a3c src/Pure/System/session.scala --- a/src/Pure/System/session.scala Mon Mar 19 21:52:09 2012 +0100 +++ b/src/Pure/System/session.scala Mon Mar 19 23:08:27 2012 +0100 @@ -24,7 +24,8 @@ //{{{ case object Global_Settings case object Caret_Focus - case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command]) + case class Commands_Changed( + assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) sealed abstract class Phase case object Inactive extends Phase @@ -227,9 +228,9 @@ object delay_commands_changed { + private var changed_assignment: Boolean = false private var changed_nodes: Set[Document.Node.Name] = Set.empty private var changed_commands: Set[Command] = Set.empty - private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty private var flush_time: Option[Long] = None @@ -241,17 +242,22 @@ def flush() { - if (changed) - commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands) + if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty) + commands_changed_buffer ! + Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands) + changed_assignment = false changed_nodes = Set.empty changed_commands = Set.empty flush_time = None } - def invoke(command: Command) + def invoke(assign: Boolean, commands: List[Command]) { - changed_nodes += command.node_name - changed_commands += command + changed_assignment |= assign + for (command <- commands) { + changed_nodes += command.node_name + changed_commands += command + } val now = System.currentTimeMillis() flush_time match { case None => flush_time = Some(now + output_delay.ms) @@ -304,22 +310,16 @@ /* exec state assignment */ def handle_assign(id: Document.Version_ID, assign: Document.Assign) - //{{{ { val cmds = global_state >>> (_.assign(id, assign)) - for (cmd <- cmds) delay_commands_changed.invoke(cmd) + delay_commands_changed.invoke(true, cmds) } - //}}} /* removed versions */ - def handle_removed(removed: List[Document.Version_ID]) - //{{{ - { + def handle_removed(removed: List[Document.Version_ID]): Unit = global_state >> (_.removed_versions(removed)) - } - //}}} /* resulting changes */ @@ -367,7 +367,7 @@ case Position.Id(state_id) if !output.is_protocol => try { val st = global_state >>> (_.accumulate(state_id, output.message)) - delay_commands_changed.invoke(st.command) + delay_commands_changed.invoke(false, List(st.command)) } catch { case _: Document.State.Fail => bad_output(output) diff -r 36dacca8a95c -r fc3bb6c02a3c src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Mon Mar 19 21:52:09 2012 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Mon Mar 19 23:08:27 2012 +0100 @@ -144,31 +144,6 @@ } - /* 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 &&= !snapshot.is_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 @@ -242,7 +217,7 @@ if (!model.buffer.isLoaded) exit_control() else Isabelle.buffer_lock(model.buffer) { - val snapshot = update_snapshot() + val snapshot = model.snapshot() if (control) init_popup(snapshot, x, y) @@ -268,7 +243,7 @@ override def getToolTipText(x: Int, y: Int): String = { robust_body(null: String) { - val snapshot = update_snapshot() + val snapshot = model.snapshot() val offset = text_area.xyToOffset(x, y) val range = Text.Range(offset, offset + 1) val tip = @@ -295,7 +270,7 @@ if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) { Isabelle.buffer_lock(model.buffer) { - val snapshot = update_snapshot() + val snapshot = model.snapshot() for (i <- 0 until physical_lines.length) { if (physical_lines(i) != -1) { val line_range = proper_line_range(start(i), end(i)) @@ -340,7 +315,7 @@ def selected_command(): Option[Command] = { Swing_Thread.require() - update_snapshot().node.command_at(text_area.getCaretPosition).map(_._1) + model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1) } private val delay_caret_update = @@ -372,16 +347,16 @@ Swing_Thread.later { Isabelle.buffer_lock(buffer) { if (model.buffer == text_area.getBuffer) { - val (updated, snapshot) = flush_snapshot() + val snapshot = model.snapshot() - if (updated || + if (changed.assignment || (changed.nodes.contains(model.name) && changed.commands.exists(snapshot.node.commands.contains))) overview.delay_repaint(true) visible_range() match { case Some(visible) => - if (updated) invalidate_range(visible) + if (changed.assignment) invalidate_range(visible) else { val visible_cmds = snapshot.node.command_range(snapshot.revert(visible)).map(_._1) diff -r 36dacca8a95c -r fc3bb6c02a3c src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Mon Mar 19 21:52:09 2012 +0100 +++ b/src/Tools/jEdit/src/output_dockable.scala Mon Mar 19 23:08:27 2012 +0100 @@ -35,7 +35,7 @@ Document_View(view.getTextArea) match { case Some(doc_view) => val cmd = current_command.get - val start_ofs = doc_view.update_snapshot().node.command_start(cmd).get + val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get val buffer = view.getBuffer buffer.beginCompoundEdit() buffer.remove(start_ofs, cmd.length) @@ -84,7 +84,7 @@ case Some(doc_view) => current_command match { case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => - val snapshot = doc_view.update_snapshot() + val snapshot = doc_view.model.snapshot() val filtered_results = snapshot.state.command_state(snapshot.version, cmd).results.iterator .map(_._2).filter( diff -r 36dacca8a95c -r fc3bb6c02a3c src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Mon Mar 19 21:52:09 2012 +0100 +++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Mar 19 23:08:27 2012 +0100 @@ -84,7 +84,7 @@ first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y: Int, line_height: Int) { - painter_snapshot = doc_view.update_snapshot() + painter_snapshot = model.snapshot() painter_clip = gfx.getClip } } diff -r 36dacca8a95c -r fc3bb6c02a3c src/Tools/jEdit/src/text_overview.scala --- a/src/Tools/jEdit/src/text_overview.scala Mon Mar 19 21:52:09 2012 +0100 +++ b/src/Tools/jEdit/src/text_overview.scala Mon Mar 19 23:08:27 2012 +0100 @@ -55,7 +55,7 @@ doc_view.robust_body(()) { Isabelle.buffer_lock(buffer) { - val snapshot = doc_view.update_snapshot() + val snapshot = doc_view.model.snapshot() gfx.setColor(getBackground) gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)