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);

--- 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 =>
                 }
+              }
             }
           }
 

--- 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 _ =>

--- 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)
       }

--- 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)
       }

--- 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))