# HG changeset patch
# User wenzelm
# Date 1377343971 -7200
# Node ID dcac8d837b9cb7bfdb81d601aef10edd888201cb
# Parent  f88635e1c52e45a83c3a6a995a1395118061e541
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;

diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -19,8 +19,6 @@
 
 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.require()
-
   private val docs = Doc.contents()
 
   private case class Documentation(name: String, title: String)
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -23,8 +23,6 @@
 
 class Find_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.require()
-
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
@@ -78,6 +76,7 @@
       react {
         case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
+
         case bad =>
           java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
       }
@@ -86,8 +85,6 @@
 
   override def init()
   {
-    Swing_Thread.require()
-
     PIDE.session.global_options += main_actor
     handle_resize()
     find_theorems.activate()
@@ -95,8 +92,6 @@
 
   override def exit()
   {
-    Swing_Thread.require()
-
     find_theorems.deactivate()
     PIDE.session.global_options -= main_actor
     delay_resize.revoke()
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -48,8 +48,6 @@
 
 class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.require()
-
   private val snapshot = Graphview_Dockable.implicit_snapshot
   private val graph = Graphview_Dockable.implicit_graph
 
@@ -82,13 +80,11 @@
 
   override def init()
   {
-    Swing_Thread.require()
     JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
   }
 
   override def exit()
   {
-    Swing_Thread.require()
     JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
   }
 }
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -51,9 +51,6 @@
 
 class Info_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.require()
-
-
   /* component state -- owned by Swing thread */
 
   private var zoom_factor = 100
@@ -108,6 +105,7 @@
       react {
         case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
+
         case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
       }
     }
@@ -115,8 +113,6 @@
 
   override def init()
   {
-    Swing_Thread.require()
-
     JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     PIDE.session.global_options += main_actor
     handle_resize()
@@ -124,8 +120,6 @@
 
   override def exit()
   {
-    Swing_Thread.require()
-
     JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
     PIDE.session.global_options -= main_actor
     delay_resize.revoke()
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -45,6 +45,7 @@
             rev_stats ::= props
             delay_update.invoke()
           }
+
         case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
       }
     }
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -23,9 +23,6 @@
 
 class Output_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.require()
-
-
   /* component state -- owned by Swing thread */
 
   private var zoom_factor = 100
@@ -91,11 +88,14 @@
       react {
         case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
+
         case changed: Session.Commands_Changed =>
           val restriction = if (changed.assignment) None else Some(changed.commands)
           Swing_Thread.later { handle_update(do_update, restriction) }
+
         case Session.Caret_Focus =>
           Swing_Thread.later { handle_update(do_update, None) }
+
         case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
       }
     }
@@ -103,8 +103,6 @@
 
   override def init()
   {
-    Swing_Thread.require()
-
     PIDE.session.global_options += main_actor
     PIDE.session.commands_changed += main_actor
     PIDE.session.caret_focus += main_actor
@@ -113,8 +111,6 @@
 
   override def exit()
   {
-    Swing_Thread.require()
-
     PIDE.session.global_options -= main_actor
     PIDE.session.commands_changed -= main_actor
     PIDE.session.caret_focus -= main_actor
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/readme_dockable.scala
--- a/src/Tools/jEdit/src/readme_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/readme_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -14,8 +14,6 @@
 
 class README_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.require()
-
   private val readme = new HTML_Panel
   private val readme_path = Path.explode("$JEDIT_HOME/README.html")
   readme.render_document(Isabelle_System.platform_file_url(readme_path), File.read(readme_path))
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -23,8 +23,6 @@
 
 class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.require()
-
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
@@ -98,9 +96,13 @@
         case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
           query_provers()
-        case Session.Ready => query_provers()
+
+        case Session.Ready =>
+          query_provers()
+
         case Sledgehammer_Params.Provers =>
           Swing_Thread.later { update_provers() }
+
         case bad =>
           java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
       }
@@ -109,8 +111,6 @@
 
   override def init()
   {
-    Swing_Thread.require()
-
     PIDE.session.phase_changed += main_actor
     PIDE.session.global_options += main_actor
     Sledgehammer_Params.provers += main_actor
@@ -121,8 +121,6 @@
 
   override def exit()
   {
-    Swing_Thread.require()
-
     sledgehammer.deactivate()
     PIDE.session.phase_changed -= main_actor
     PIDE.session.global_options -= main_actor
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/syslog_dockable.scala
--- a/src/Tools/jEdit/src/syslog_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -23,10 +23,10 @@
 
   private def update_syslog()
   {
-    Swing_Thread.later {
-      val text = PIDE.session.current_syslog()
-      if (text != syslog.text) syslog.text = text
-    }
+    Swing_Thread.require()
+
+    val text = PIDE.session.current_syslog()
+    if (text != syslog.text) syslog.text = text
   }
 
   set_content(syslog)
@@ -38,7 +38,7 @@
     loop {
       react {
         case output: Isabelle_Process.Output =>
-          if (output.is_syslog) update_syslog()
+          if (output.is_syslog) Swing_Thread.later { update_syslog() }
 
         case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
       }
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -69,7 +69,8 @@
 
   private def handle_phase(phase: Session.Phase)
   {
-    Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
+    Swing_Thread.require()
+    session_phase.text = " " + phase_text(phase) + " "
   }
 
   private val continuous_checking = new CheckBox("Continuous checking") {
@@ -183,25 +184,25 @@
 
   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
-    Swing_Thread.now {
-      val snapshot = PIDE.session.snapshot()
+    Swing_Thread.require()
+
+    val snapshot = PIDE.session.snapshot()
 
-      val iterator =
-        restriction match {
-          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
-          case None => snapshot.version.nodes.entries
-        }
-      val nodes_status1 =
-        (nodes_status /: iterator)({ case (status, (name, node)) =>
-            if (PIDE.thy_load.loaded_theories(name.theory)) status
-            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
+    val iterator =
+      restriction match {
+        case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
+        case None => snapshot.version.nodes.entries
+      }
+    val nodes_status1 =
+      (nodes_status /: iterator)({ case (status, (name, node)) =>
+          if (PIDE.thy_load.loaded_theories(name.theory)) status
+          else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
-      if (nodes_status != nodes_status1) {
-        nodes_status = nodes_status1
-        status.listData =
-          snapshot.version.nodes.topological_order.filter(
-            (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
-      }
+    if (nodes_status != nodes_status1) {
+      nodes_status = nodes_status1
+      status.listData =
+        snapshot.version.nodes.topological_order.filter(
+          (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
     }
   }
 
@@ -211,7 +212,8 @@
   private val main_actor = actor {
     loop {
       react {
-        case phase: Session.Phase => handle_phase(phase)
+        case phase: Session.Phase =>
+          Swing_Thread.later { handle_phase(phase) }
 
         case _: Session.Global_Options =>
           Swing_Thread.later {
@@ -221,7 +223,8 @@
             status.repaint()
           }
 
-        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
+        case changed: Session.Commands_Changed =>
+          Swing_Thread.later { handle_update(Some(changed.nodes)) }
 
         case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
       }
@@ -230,9 +233,12 @@
 
   override def init()
   {
-    PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase)
+    PIDE.session.phase_changed += main_actor
     PIDE.session.global_options += main_actor
-    PIDE.session.commands_changed += main_actor; handle_update()
+    PIDE.session.commands_changed += main_actor
+
+    handle_phase(PIDE.session.phase)
+    handle_update()
   }
 
   override def exit()
diff -r f88635e1c52e -r dcac8d837b9c src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -175,28 +175,28 @@
 
   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
-    Swing_Thread.now {
-      val snapshot = PIDE.session.snapshot()
+    Swing_Thread.require()
+
+    val snapshot = PIDE.session.snapshot()
 
-      val iterator =
-        restriction match {
-          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
-          case None => snapshot.version.nodes.entries
-        }
-      val nodes_timing1 =
-        (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
-            if (PIDE.thy_load.loaded_theories(name.theory)) timing1
-            else {
-              val node_timing =
-                Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
-              timing1 + (name -> node_timing)
-            }
-        })
-      nodes_timing = nodes_timing1
+    val iterator =
+      restriction match {
+        case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
+        case None => snapshot.version.nodes.entries
+      }
+    val nodes_timing1 =
+      (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
+          if (PIDE.thy_load.loaded_theories(name.theory)) timing1
+          else {
+            val node_timing =
+              Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
+            timing1 + (name -> node_timing)
+          }
+      })
+    nodes_timing = nodes_timing1
 
-      val entries = make_entries()
-      if (timing_view.listData.toList != entries) timing_view.listData = entries
-    }
+    val entries = make_entries()
+    if (timing_view.listData.toList != entries) timing_view.listData = entries
   }
 
 
@@ -205,7 +205,8 @@
   private val main_actor = actor {
     loop {
       react {
-        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
+        case changed: Session.Commands_Changed =>
+          Swing_Thread.later { handle_update(Some(changed.nodes)) }
 
         case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
       }