node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
authorwenzelm
Mon, 04 Jan 2016 21:42:32 +0100
changeset 62052 8bcbf1c93119
parent 62051 c3c871b509d9
child 62053 1c8252d07e32
node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Jan 04 20:34:34 2016 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Jan 04 21:42:32 2016 +0100
@@ -192,9 +192,9 @@
 
   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
-    val (snapshot, nodes_status0) =
-      GUI_Thread.now { (PIDE.session.snapshot(), nodes_status) }
+    GUI_Thread.require {}
 
+    val snapshot = PIDE.session.snapshot()
     val nodes = snapshot.version.nodes
 
     val iterator =
@@ -203,7 +203,7 @@
         case None => nodes.iterator
       }
     val nodes_status1 =
-      (nodes_status0 /: iterator)({ case (status, (name, node)) =>
+      (nodes_status /: iterator)({ case (status, (name, node)) =>
           if (!name.is_theory || PIDE.resources.loaded_theories(name.theory) || node.is_empty)
             status
           else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
@@ -211,12 +211,10 @@
     val nodes_status2 =
       nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_))
 
-    if (nodes_status0 != nodes_status2)
-      GUI_Thread.now {
-        nodes_status = nodes_status2
-        status.listData = nodes.topological_order.filter(nodes_status.isDefinedAt(_))
-        status.repaint()
-      }
+    if (nodes_status != nodes_status2) {
+      nodes_status = nodes_status2
+      status.listData = nodes.topological_order.filter(nodes_status.isDefinedAt(_))
+    }
   }
 
 
@@ -236,7 +234,7 @@
         }
 
       case changed: Session.Commands_Changed =>
-        handle_update(Some(changed.nodes))
+        GUI_Thread.later { handle_update(Some(changed.nodes)) }
     }
 
   override def init()