merged

--- a/src/HOL/Library/Product_Order.thy	Mon Jan 04 17:45:36 2016 +0100
+++ b/src/HOL/Library/Product_Order.thy	Mon Jan 04 22:13:53 2016 +0100
@@ -153,7 +153,7 @@
 instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
 
 instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
-  by standard (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
+  by standard (auto simp add: prod_eqI diff_eq)
 
 
 subsection \<open>Complete lattice operations\<close>
@@ -179,7 +179,8 @@
 instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
     conditionally_complete_lattice
   by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
-    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
+    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq
+    intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
 
 instance prod :: (complete_lattice, complete_lattice) complete_lattice
   by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def

--- a/src/Pure/PIDE/session.scala	Mon Jan 04 17:45:36 2016 +0100
+++ b/src/Pure/PIDE/session.scala	Mon Jan 04 22:13:53 2016 +0100
@@ -605,11 +605,11 @@
 
   def stop()
   {
+    delay_prune.revoke()
     manager.send_wait(Stop)
     prover.await_reset()
     change_parser.shutdown()
     change_buffer.shutdown()
-    delay_prune.revoke()
     manager.shutdown()
     dispatcher.shutdown()
   }

--- a/src/Pure/Tools/debugger.scala	Mon Jan 04 17:45:36 2016 +0100
+++ b/src/Pure/Tools/debugger.scala	Mon Jan 04 22:13:53 2016 +0100
@@ -61,7 +61,10 @@
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
   {
     def set_session(new_session: Session): State =
+    {
+      session.stop()
       copy(session = new_session)
+    }
 
     def set_break(b: Boolean): State = copy(break = b)
 

--- a/src/Tools/jEdit/src/plugin.scala	Mon Jan 04 17:45:36 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Jan 04 22:13:53 2016 +0100
@@ -398,6 +398,7 @@
       val resources =
         new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
 
+      PIDE.session.stop()
       PIDE.session = new Session(resources) {
         override def output_delay = PIDE.options.seconds("editor_output_delay")
         override def prune_delay = PIDE.options.seconds("editor_prune_delay")

--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Jan 04 17:45:36 2016 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Jan 04 22:13:53 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()