# HG changeset patch
# User wenzelm
# Date 1444047440 -7200
# Node ID 3ad2b2055ffc968b065c930762ff30456d7b828a
# Parent  44f4ffe2b210c49f62bf7e37289a7049488ccb6b
produce nodes_status outside GUI thread, to avoid a few milliseconds of blocking;

diff -r 44f4ffe2b210 -r 3ad2b2055ffc src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Oct 04 17:48:34 2015 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Oct 05 14:17:20 2015 +0200
@@ -192,9 +192,9 @@
 
   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
-    GUI_Thread.require {}
+    val (snapshot, nodes_status0) =
+      GUI_Thread.now { (PIDE.session.snapshot(), nodes_status) }
 
-    val snapshot = PIDE.session.snapshot()
     val nodes = snapshot.version.nodes
 
     val iterator =
@@ -203,7 +203,7 @@
         case None => nodes.iterator
       }
     val nodes_status1 =
-      (nodes_status /: iterator)({ case (status, (name, node)) =>
+      (nodes_status0 /: 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,10 +211,12 @@
     val nodes_status2 =
       nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_))
 
-    if (nodes_status != nodes_status2) {
-      nodes_status = nodes_status2
-      status.listData = nodes.topological_order.filter(nodes_status.isDefinedAt(_))
-    }
+    if (nodes_status0 != nodes_status2)
+      GUI_Thread.now {
+        nodes_status = nodes_status2
+        status.listData = nodes.topological_order.filter(nodes_status.isDefinedAt(_))
+        status.repaint
+      }
   }
 
 
@@ -234,7 +236,7 @@
         }
 
       case changed: Session.Commands_Changed =>
-        GUI_Thread.later { handle_update(Some(changed.nodes)) }
+        handle_update(Some(changed.nodes))
     }
 
   override def init()