# HG changeset patch # User wenzelm # Date 1451940152 -3600 # Node ID 8bcbf1c93119b679bc94b76ae17e923b3c71b6ae # Parent c3c871b509d963383d3d0e698fab286d5585671d 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; diff -r c3c871b509d9 -r 8bcbf1c93119 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()