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;
--- 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()