# HG changeset patch
# User wenzelm
# Date 1444061038 -7200
# Node ID fa7a46489285281a6a7c96d76e859ba9e810ac3f
# Parent  1cfc476198c937820239c0c40e7b826168ae7e46# Parent  0a4c364df4312ceb07951b9736f2e014ace45472
merged

diff -r 1cfc476198c9 -r fa7a46489285 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Oct 05 16:14:33 2015 +0200
+++ b/src/Provers/classical.ML	Mon Oct 05 18:03:58 2015 +0200
@@ -119,6 +119,8 @@
   val unsafe_elim: int option -> attribute
   val unsafe_intro: int option -> attribute
   val rule_del: attribute
+  val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
+  val standard_tac: Proof.context -> thm list -> tactic
   val cla_modifiers: Method.modifier parser list
   val cla_method:
     (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
diff -r 1cfc476198c9 -r fa7a46489285 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Oct 05 16:14:33 2015 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Oct 05 18:03:58 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()