# HG changeset patch # User wenzelm # Date 1331734173 -3600 # Node ID 1752164d916b6eb355fe504bf9a6fc7b80010af6 # Parent 2f6c1952188af1b2cc4f2e188d0b9a26a592321a prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks; more robust use of Session.Commands_Changed vs. Document_View.visible_range as asynchronous swing task, taking into account that the model might have switched in the meantime (e.g. via fast clicking on hypersearch while the prover is crunching); diff -r 2f6c1952188a -r 1752164d916b src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Wed Mar 14 14:49:43 2012 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Wed Mar 14 15:09:33 2012 +0100 @@ -365,32 +365,36 @@ react { case changed: Session.Commands_Changed => val buffer = model.buffer - Isabelle.swing_buffer_lock(buffer) { - val (updated, snapshot) = flush_snapshot() + Swing_Thread.later { + Isabelle.buffer_lock(buffer) { + if (model.buffer == text_area.getBuffer) { + val (updated, snapshot) = flush_snapshot() - if (updated || - (changed.nodes.contains(model.name) && - changed.commands.exists(snapshot.node.commands.contains))) - overview.delay_repaint(true) + if (updated || + (changed.nodes.contains(model.name) && + changed.commands.exists(snapshot.node.commands.contains))) + overview.delay_repaint(true) - visible_range() match { - case None => - case Some(visible) => - if (updated) invalidate_range(visible) - else { - val visible_cmds = - snapshot.node.command_range(snapshot.revert(visible)).map(_._1) - if (visible_cmds.exists(changed.commands)) { - 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.commands) - } text_area.invalidateScreenLineRange(line, line) - } + visible_range() match { + case Some(visible) => + if (updated) invalidate_range(visible) + else { + val visible_cmds = + snapshot.node.command_range(snapshot.revert(visible)).map(_._1) + if (visible_cmds.exists(changed.commands)) { + 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.commands) + } text_area.invalidateScreenLineRange(line, line) + } + } + case None => } + } } } diff -r 2f6c1952188a -r 1752164d916b src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Mar 14 14:49:43 2012 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Wed Mar 14 15:09:33 2012 +0100 @@ -386,7 +386,7 @@ case phase: Session.Phase => phase match { case Session.Failed => - Swing_Thread.now { + Swing_Thread.later { val text = new scala.swing.TextArea(Isabelle.session.current_syslog()) text.editable = false Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text) @@ -445,7 +445,7 @@ } case msg: PropertiesChanged => - Swing_Thread.now { Isabelle.setup_tooltips() } + Isabelle.setup_tooltips() Isabelle.session.global_settings.event(Session.Global_Settings) case _ => diff -r 2f6c1952188a -r 1752164d916b src/Tools/jEdit/src/protocol_dockable.scala --- a/src/Tools/jEdit/src/protocol_dockable.scala Wed Mar 14 14:49:43 2012 +0100 +++ b/src/Tools/jEdit/src/protocol_dockable.scala Wed Mar 14 15:09:33 2012 +0100 @@ -29,10 +29,10 @@ loop { react { case input: Isabelle_Process.Input => - Swing_Thread.now { text_area.append(input.toString + "\n") } + Swing_Thread.later { text_area.append(input.toString + "\n") } case output: Isabelle_Process.Output => - Swing_Thread.now { text_area.append(output.message.toString + "\n") } + Swing_Thread.later { text_area.append(output.message.toString + "\n") } case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad) } diff -r 2f6c1952188a -r 1752164d916b src/Tools/jEdit/src/raw_output_dockable.scala --- a/src/Tools/jEdit/src/raw_output_dockable.scala Wed Mar 14 14:49:43 2012 +0100 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala Wed Mar 14 15:09:33 2012 +0100 @@ -31,7 +31,7 @@ react { case output: Isabelle_Process.Output => if (output.is_stdout || output.is_stderr) - Swing_Thread.now { text_area.append(XML.content(output.message).mkString) } + Swing_Thread.later { text_area.append(XML.content(output.message).mkString) } case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) } diff -r 2f6c1952188a -r 1752164d916b src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Wed Mar 14 14:49:43 2012 +0100 +++ b/src/Tools/jEdit/src/session_dockable.scala Wed Mar 14 15:09:33 2012 +0100 @@ -175,13 +175,13 @@ react { case output: Isabelle_Process.Output => if (output.is_syslog) - Swing_Thread.now { + Swing_Thread.later { val text = Isabelle.session.current_syslog() if (text != syslog.text) syslog.text = text } case phase: Session.Phase => - Swing_Thread.now { session_phase.text = " " + phase.toString + " " } + Swing_Thread.later { session_phase.text = " " + phase.toString + " " } case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))