prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
authorwenzelm
Wed Mar 14 15:09:33 2012 +0100 (2012-03-14)
changeset 469181752164d916b
parent 46917 2f6c1952188a
child 46919 82fc322fc30a
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);
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/protocol_dockable.scala
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Mar 14 14:49:43 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Mar 14 15:09:33 2012 +0100
     1.3 @@ -365,32 +365,36 @@
     1.4        react {
     1.5          case changed: Session.Commands_Changed =>
     1.6            val buffer = model.buffer
     1.7 -          Isabelle.swing_buffer_lock(buffer) {
     1.8 -            val (updated, snapshot) = flush_snapshot()
     1.9 +          Swing_Thread.later {
    1.10 +            Isabelle.buffer_lock(buffer) {
    1.11 +              if (model.buffer == text_area.getBuffer) {
    1.12 +                val (updated, snapshot) = flush_snapshot()
    1.13  
    1.14 -            if (updated ||
    1.15 -                (changed.nodes.contains(model.name) &&
    1.16 -                 changed.commands.exists(snapshot.node.commands.contains)))
    1.17 -              overview.delay_repaint(true)
    1.18 +                if (updated ||
    1.19 +                    (changed.nodes.contains(model.name) &&
    1.20 +                     changed.commands.exists(snapshot.node.commands.contains)))
    1.21 +                  overview.delay_repaint(true)
    1.22  
    1.23 -            visible_range() match {
    1.24 -              case None =>
    1.25 -              case Some(visible) =>
    1.26 -                if (updated) invalidate_range(visible)
    1.27 -                else {
    1.28 -                  val visible_cmds =
    1.29 -                    snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
    1.30 -                  if (visible_cmds.exists(changed.commands)) {
    1.31 -                    for {
    1.32 -                      line <- 0 until text_area.getVisibleLines
    1.33 -                      val start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.34 -                      val end = text_area.getScreenLineEndOffset(line) if end >= 0
    1.35 -                      val range = proper_line_range(start, end)
    1.36 -                      val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    1.37 -                      if line_cmds.exists(changed.commands)
    1.38 -                    } text_area.invalidateScreenLineRange(line, line)
    1.39 -                  }
    1.40 +                visible_range() match {
    1.41 +                  case Some(visible) =>
    1.42 +                    if (updated) invalidate_range(visible)
    1.43 +                    else {
    1.44 +                      val visible_cmds =
    1.45 +                        snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
    1.46 +                      if (visible_cmds.exists(changed.commands)) {
    1.47 +                        for {
    1.48 +                          line <- 0 until text_area.getVisibleLines
    1.49 +                          val start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.50 +                          val end = text_area.getScreenLineEndOffset(line) if end >= 0
    1.51 +                          val range = proper_line_range(start, end)
    1.52 +                          val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    1.53 +                          if line_cmds.exists(changed.commands)
    1.54 +                        } text_area.invalidateScreenLineRange(line, line)
    1.55 +                      }
    1.56 +                    }
    1.57 +                  case None =>
    1.58                  }
    1.59 +              }
    1.60              }
    1.61            }
    1.62  
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 14 14:49:43 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 14 15:09:33 2012 +0100
     2.3 @@ -386,7 +386,7 @@
     2.4          case phase: Session.Phase =>
     2.5            phase match {
     2.6              case Session.Failed =>
     2.7 -              Swing_Thread.now {
     2.8 +              Swing_Thread.later {
     2.9                  val text = new scala.swing.TextArea(Isabelle.session.current_syslog())
    2.10                  text.editable = false
    2.11                  Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
    2.12 @@ -445,7 +445,7 @@
    2.13          }
    2.14  
    2.15        case msg: PropertiesChanged =>
    2.16 -        Swing_Thread.now { Isabelle.setup_tooltips() }
    2.17 +        Isabelle.setup_tooltips()
    2.18          Isabelle.session.global_settings.event(Session.Global_Settings)
    2.19  
    2.20        case _ =>
     3.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Wed Mar 14 14:49:43 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Wed Mar 14 15:09:33 2012 +0100
     3.3 @@ -29,10 +29,10 @@
     3.4      loop {
     3.5        react {
     3.6          case input: Isabelle_Process.Input =>
     3.7 -          Swing_Thread.now { text_area.append(input.toString + "\n") }
     3.8 +          Swing_Thread.later { text_area.append(input.toString + "\n") }
     3.9  
    3.10          case output: Isabelle_Process.Output =>
    3.11 -          Swing_Thread.now { text_area.append(output.message.toString + "\n") }
    3.12 +          Swing_Thread.later { text_area.append(output.message.toString + "\n") }
    3.13  
    3.14          case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
    3.15        }
     4.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Wed Mar 14 14:49:43 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Wed Mar 14 15:09:33 2012 +0100
     4.3 @@ -31,7 +31,7 @@
     4.4        react {
     4.5          case output: Isabelle_Process.Output =>
     4.6            if (output.is_stdout || output.is_stderr)
     4.7 -            Swing_Thread.now { text_area.append(XML.content(output.message).mkString) }
     4.8 +            Swing_Thread.later { text_area.append(XML.content(output.message).mkString) }
     4.9  
    4.10          case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
    4.11        }
     5.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Wed Mar 14 14:49:43 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Mar 14 15:09:33 2012 +0100
     5.3 @@ -175,13 +175,13 @@
     5.4        react {
     5.5          case output: Isabelle_Process.Output =>
     5.6            if (output.is_syslog)
     5.7 -            Swing_Thread.now {
     5.8 +            Swing_Thread.later {
     5.9                val text = Isabelle.session.current_syslog()
    5.10                if (text != syslog.text) syslog.text = text
    5.11              }
    5.12  
    5.13          case phase: Session.Phase =>
    5.14 -          Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
    5.15 +          Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
    5.16  
    5.17          case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
    5.18