more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
authorwenzelm
Sat Aug 24 13:32:51 2013 +0200 (2013-08-24)
changeset 53177dcac8d837b9c
parent 53176 f88635e1c52e
child 53178 0a3a5f606b2a
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
src/Tools/jEdit/src/documentation_dockable.scala
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/monitor_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/readme_dockable.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
src/Tools/jEdit/src/syslog_dockable.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     1.3 @@ -19,8 +19,6 @@
     1.4  
     1.5  class Documentation_Dockable(view: View, position: String) extends Dockable(view, position)
     1.6  {
     1.7 -  Swing_Thread.require()
     1.8 -
     1.9    private val docs = Doc.contents()
    1.10  
    1.11    private case class Documentation(name: String, title: String)
     2.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     2.3 @@ -23,8 +23,6 @@
     2.4  
     2.5  class Find_Dockable(view: View, position: String) extends Dockable(view, position)
     2.6  {
     2.7 -  Swing_Thread.require()
     2.8 -
     2.9    val pretty_text_area = new Pretty_Text_Area(view)
    2.10    set_content(pretty_text_area)
    2.11  
    2.12 @@ -78,6 +76,7 @@
    2.13        react {
    2.14          case _: Session.Global_Options =>
    2.15            Swing_Thread.later { handle_resize() }
    2.16 +
    2.17          case bad =>
    2.18            java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
    2.19        }
    2.20 @@ -86,8 +85,6 @@
    2.21  
    2.22    override def init()
    2.23    {
    2.24 -    Swing_Thread.require()
    2.25 -
    2.26      PIDE.session.global_options += main_actor
    2.27      handle_resize()
    2.28      find_theorems.activate()
    2.29 @@ -95,8 +92,6 @@
    2.30  
    2.31    override def exit()
    2.32    {
    2.33 -    Swing_Thread.require()
    2.34 -
    2.35      find_theorems.deactivate()
    2.36      PIDE.session.global_options -= main_actor
    2.37      delay_resize.revoke()
     3.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     3.3 @@ -48,8 +48,6 @@
     3.4  
     3.5  class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
     3.6  {
     3.7 -  Swing_Thread.require()
     3.8 -
     3.9    private val snapshot = Graphview_Dockable.implicit_snapshot
    3.10    private val graph = Graphview_Dockable.implicit_graph
    3.11  
    3.12 @@ -82,13 +80,11 @@
    3.13  
    3.14    override def init()
    3.15    {
    3.16 -    Swing_Thread.require()
    3.17      JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
    3.18    }
    3.19  
    3.20    override def exit()
    3.21    {
    3.22 -    Swing_Thread.require()
    3.23      JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
    3.24    }
    3.25  }
     4.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     4.3 @@ -51,9 +51,6 @@
     4.4  
     4.5  class Info_Dockable(view: View, position: String) extends Dockable(view, position)
     4.6  {
     4.7 -  Swing_Thread.require()
     4.8 -
     4.9 -
    4.10    /* component state -- owned by Swing thread */
    4.11  
    4.12    private var zoom_factor = 100
    4.13 @@ -108,6 +105,7 @@
    4.14        react {
    4.15          case _: Session.Global_Options =>
    4.16            Swing_Thread.later { handle_resize() }
    4.17 +
    4.18          case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
    4.19        }
    4.20      }
    4.21 @@ -115,8 +113,6 @@
    4.22  
    4.23    override def init()
    4.24    {
    4.25 -    Swing_Thread.require()
    4.26 -
    4.27      JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
    4.28      PIDE.session.global_options += main_actor
    4.29      handle_resize()
    4.30 @@ -124,8 +120,6 @@
    4.31  
    4.32    override def exit()
    4.33    {
    4.34 -    Swing_Thread.require()
    4.35 -
    4.36      JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
    4.37      PIDE.session.global_options -= main_actor
    4.38      delay_resize.revoke()
     5.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     5.3 @@ -45,6 +45,7 @@
     5.4              rev_stats ::= props
     5.5              delay_update.invoke()
     5.6            }
     5.7 +
     5.8          case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
     5.9        }
    5.10      }
     6.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     6.3 @@ -23,9 +23,6 @@
     6.4  
     6.5  class Output_Dockable(view: View, position: String) extends Dockable(view, position)
     6.6  {
     6.7 -  Swing_Thread.require()
     6.8 -
     6.9 -
    6.10    /* component state -- owned by Swing thread */
    6.11  
    6.12    private var zoom_factor = 100
    6.13 @@ -91,11 +88,14 @@
    6.14        react {
    6.15          case _: Session.Global_Options =>
    6.16            Swing_Thread.later { handle_resize() }
    6.17 +
    6.18          case changed: Session.Commands_Changed =>
    6.19            val restriction = if (changed.assignment) None else Some(changed.commands)
    6.20            Swing_Thread.later { handle_update(do_update, restriction) }
    6.21 +
    6.22          case Session.Caret_Focus =>
    6.23            Swing_Thread.later { handle_update(do_update, None) }
    6.24 +
    6.25          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    6.26        }
    6.27      }
    6.28 @@ -103,8 +103,6 @@
    6.29  
    6.30    override def init()
    6.31    {
    6.32 -    Swing_Thread.require()
    6.33 -
    6.34      PIDE.session.global_options += main_actor
    6.35      PIDE.session.commands_changed += main_actor
    6.36      PIDE.session.caret_focus += main_actor
    6.37 @@ -113,8 +111,6 @@
    6.38  
    6.39    override def exit()
    6.40    {
    6.41 -    Swing_Thread.require()
    6.42 -
    6.43      PIDE.session.global_options -= main_actor
    6.44      PIDE.session.commands_changed -= main_actor
    6.45      PIDE.session.caret_focus -= main_actor
     7.1 --- a/src/Tools/jEdit/src/readme_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     7.2 +++ b/src/Tools/jEdit/src/readme_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     7.3 @@ -14,8 +14,6 @@
     7.4  
     7.5  class README_Dockable(view: View, position: String) extends Dockable(view, position)
     7.6  {
     7.7 -  Swing_Thread.require()
     7.8 -
     7.9    private val readme = new HTML_Panel
    7.10    private val readme_path = Path.explode("$JEDIT_HOME/README.html")
    7.11    readme.render_document(Isabelle_System.platform_file_url(readme_path), File.read(readme_path))
     8.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     8.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     8.3 @@ -23,8 +23,6 @@
     8.4  
     8.5  class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position)
     8.6  {
     8.7 -  Swing_Thread.require()
     8.8 -
     8.9    val pretty_text_area = new Pretty_Text_Area(view)
    8.10    set_content(pretty_text_area)
    8.11  
    8.12 @@ -98,9 +96,13 @@
    8.13          case _: Session.Global_Options =>
    8.14            Swing_Thread.later { handle_resize() }
    8.15            query_provers()
    8.16 -        case Session.Ready => query_provers()
    8.17 +
    8.18 +        case Session.Ready =>
    8.19 +          query_provers()
    8.20 +
    8.21          case Sledgehammer_Params.Provers =>
    8.22            Swing_Thread.later { update_provers() }
    8.23 +
    8.24          case bad =>
    8.25            java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
    8.26        }
    8.27 @@ -109,8 +111,6 @@
    8.28  
    8.29    override def init()
    8.30    {
    8.31 -    Swing_Thread.require()
    8.32 -
    8.33      PIDE.session.phase_changed += main_actor
    8.34      PIDE.session.global_options += main_actor
    8.35      Sledgehammer_Params.provers += main_actor
    8.36 @@ -121,8 +121,6 @@
    8.37  
    8.38    override def exit()
    8.39    {
    8.40 -    Swing_Thread.require()
    8.41 -
    8.42      sledgehammer.deactivate()
    8.43      PIDE.session.phase_changed -= main_actor
    8.44      PIDE.session.global_options -= main_actor
     9.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
     9.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
     9.3 @@ -23,10 +23,10 @@
     9.4  
     9.5    private def update_syslog()
     9.6    {
     9.7 -    Swing_Thread.later {
     9.8 -      val text = PIDE.session.current_syslog()
     9.9 -      if (text != syslog.text) syslog.text = text
    9.10 -    }
    9.11 +    Swing_Thread.require()
    9.12 +
    9.13 +    val text = PIDE.session.current_syslog()
    9.14 +    if (text != syslog.text) syslog.text = text
    9.15    }
    9.16  
    9.17    set_content(syslog)
    9.18 @@ -38,7 +38,7 @@
    9.19      loop {
    9.20        react {
    9.21          case output: Isabelle_Process.Output =>
    9.22 -          if (output.is_syslog) update_syslog()
    9.23 +          if (output.is_syslog) Swing_Thread.later { update_syslog() }
    9.24  
    9.25          case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
    9.26        }
    10.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
    10.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
    10.3 @@ -69,7 +69,8 @@
    10.4  
    10.5    private def handle_phase(phase: Session.Phase)
    10.6    {
    10.7 -    Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
    10.8 +    Swing_Thread.require()
    10.9 +    session_phase.text = " " + phase_text(phase) + " "
   10.10    }
   10.11  
   10.12    private val continuous_checking = new CheckBox("Continuous checking") {
   10.13 @@ -183,25 +184,25 @@
   10.14  
   10.15    private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   10.16    {
   10.17 -    Swing_Thread.now {
   10.18 -      val snapshot = PIDE.session.snapshot()
   10.19 +    Swing_Thread.require()
   10.20 +
   10.21 +    val snapshot = PIDE.session.snapshot()
   10.22  
   10.23 -      val iterator =
   10.24 -        restriction match {
   10.25 -          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
   10.26 -          case None => snapshot.version.nodes.entries
   10.27 -        }
   10.28 -      val nodes_status1 =
   10.29 -        (nodes_status /: iterator)({ case (status, (name, node)) =>
   10.30 -            if (PIDE.thy_load.loaded_theories(name.theory)) status
   10.31 -            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
   10.32 +    val iterator =
   10.33 +      restriction match {
   10.34 +        case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
   10.35 +        case None => snapshot.version.nodes.entries
   10.36 +      }
   10.37 +    val nodes_status1 =
   10.38 +      (nodes_status /: iterator)({ case (status, (name, node)) =>
   10.39 +          if (PIDE.thy_load.loaded_theories(name.theory)) status
   10.40 +          else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
   10.41  
   10.42 -      if (nodes_status != nodes_status1) {
   10.43 -        nodes_status = nodes_status1
   10.44 -        status.listData =
   10.45 -          snapshot.version.nodes.topological_order.filter(
   10.46 -            (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
   10.47 -      }
   10.48 +    if (nodes_status != nodes_status1) {
   10.49 +      nodes_status = nodes_status1
   10.50 +      status.listData =
   10.51 +        snapshot.version.nodes.topological_order.filter(
   10.52 +          (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
   10.53      }
   10.54    }
   10.55  
   10.56 @@ -211,7 +212,8 @@
   10.57    private val main_actor = actor {
   10.58      loop {
   10.59        react {
   10.60 -        case phase: Session.Phase => handle_phase(phase)
   10.61 +        case phase: Session.Phase =>
   10.62 +          Swing_Thread.later { handle_phase(phase) }
   10.63  
   10.64          case _: Session.Global_Options =>
   10.65            Swing_Thread.later {
   10.66 @@ -221,7 +223,8 @@
   10.67              status.repaint()
   10.68            }
   10.69  
   10.70 -        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
   10.71 +        case changed: Session.Commands_Changed =>
   10.72 +          Swing_Thread.later { handle_update(Some(changed.nodes)) }
   10.73  
   10.74          case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
   10.75        }
   10.76 @@ -230,9 +233,12 @@
   10.77  
   10.78    override def init()
   10.79    {
   10.80 -    PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase)
   10.81 +    PIDE.session.phase_changed += main_actor
   10.82      PIDE.session.global_options += main_actor
   10.83 -    PIDE.session.commands_changed += main_actor; handle_update()
   10.84 +    PIDE.session.commands_changed += main_actor
   10.85 +
   10.86 +    handle_phase(PIDE.session.phase)
   10.87 +    handle_update()
   10.88    }
   10.89  
   10.90    override def exit()
    11.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
    11.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
    11.3 @@ -175,28 +175,28 @@
    11.4  
    11.5    private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
    11.6    {
    11.7 -    Swing_Thread.now {
    11.8 -      val snapshot = PIDE.session.snapshot()
    11.9 +    Swing_Thread.require()
   11.10 +
   11.11 +    val snapshot = PIDE.session.snapshot()
   11.12  
   11.13 -      val iterator =
   11.14 -        restriction match {
   11.15 -          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
   11.16 -          case None => snapshot.version.nodes.entries
   11.17 -        }
   11.18 -      val nodes_timing1 =
   11.19 -        (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
   11.20 -            if (PIDE.thy_load.loaded_theories(name.theory)) timing1
   11.21 -            else {
   11.22 -              val node_timing =
   11.23 -                Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
   11.24 -              timing1 + (name -> node_timing)
   11.25 -            }
   11.26 -        })
   11.27 -      nodes_timing = nodes_timing1
   11.28 +    val iterator =
   11.29 +      restriction match {
   11.30 +        case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
   11.31 +        case None => snapshot.version.nodes.entries
   11.32 +      }
   11.33 +    val nodes_timing1 =
   11.34 +      (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
   11.35 +          if (PIDE.thy_load.loaded_theories(name.theory)) timing1
   11.36 +          else {
   11.37 +            val node_timing =
   11.38 +              Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
   11.39 +            timing1 + (name -> node_timing)
   11.40 +          }
   11.41 +      })
   11.42 +    nodes_timing = nodes_timing1
   11.43  
   11.44 -      val entries = make_entries()
   11.45 -      if (timing_view.listData.toList != entries) timing_view.listData = entries
   11.46 -    }
   11.47 +    val entries = make_entries()
   11.48 +    if (timing_view.listData.toList != entries) timing_view.listData = entries
   11.49    }
   11.50  
   11.51  
   11.52 @@ -205,7 +205,8 @@
   11.53    private val main_actor = actor {
   11.54      loop {
   11.55        react {
   11.56 -        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
   11.57 +        case changed: Session.Commands_Changed =>
   11.58 +          Swing_Thread.later { handle_update(Some(changed.nodes)) }
   11.59  
   11.60          case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
   11.61        }