# HG changeset patch
# User wenzelm
# Date 1489446818 -3600
# Node ID 420f55912b3e70fb0c7c88b5e335087bdeb0210f
# Parent  ed4b47b8c7dc015dc852c2931873aa862d61e4d4
tuned;

diff -r ed4b47b8c7dc -r 420f55912b3e src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Tue Mar 14 00:09:15 2017 +0100
+++ b/src/Pure/System/invoke_scala.scala	Tue Mar 14 00:13:38 2017 +0100
@@ -77,6 +77,12 @@
   override def init(init_session: Session): Unit =
     synchronized { session = init_session }
 
+  override def exit(): Unit = synchronized
+  {
+    for ((id, future) <- futures) cancel(id, future)
+    futures = Map.empty
+  }
+
   private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
     synchronized
     {
@@ -119,12 +125,6 @@
     }
   }
 
-  override def exit(): Unit = synchronized
-  {
-    for ((id, future) <- futures) cancel(id, future)
-    futures = Map.empty
-  }
-
   val functions =
     List(
       Markup.INVOKE_SCALA -> invoke_scala _,
diff -r ed4b47b8c7dc -r 420f55912b3e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 14 00:09:15 2017 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 14 00:13:38 2017 +0100
@@ -806,6 +806,9 @@
   {
     private val pending = Synchronized(Map.empty[String, Promise[XML.Body]])
 
+    override def exit(): Unit =
+      pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
+
     def build_theories(
       session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
     {
@@ -839,9 +842,6 @@
         case _ => false
       }
 
-    override def exit(): Unit =
-      pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
-
     val functions =
       List(
         Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
diff -r ed4b47b8c7dc -r 420f55912b3e src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Tue Mar 14 00:09:15 2017 +0100
+++ b/src/Pure/Tools/print_operation.scala	Tue Mar 14 00:13:38 2017 +0100
@@ -22,6 +22,9 @@
   {
     private val print_operations = Synchronized[List[(String, String)]](Nil)
 
+    override def init(session: Session): Unit =
+      session.protocol_command(Markup.PRINT_OPERATIONS)
+
     def get: List[(String, String)] = print_operations.value
 
     private def put(msg: Prover.Protocol_Output): Boolean =
@@ -35,9 +38,6 @@
       true
     }
 
-    override def init(session: Session): Unit =
-      session.protocol_command(Markup.PRINT_OPERATIONS)
-
     val functions = List(Markup.PRINT_OPERATIONS -> put _)
   }
 }
diff -r ed4b47b8c7dc -r 420f55912b3e src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Tue Mar 14 00:09:15 2017 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala	Tue Mar 14 00:13:38 2017 +0100
@@ -290,6 +290,12 @@
   {
     assert(manager.is_active)
 
+    override def exit() =
+    {
+      manager.send(Clear_Memory)
+      manager.shutdown()
+    }
+
     private def cancel(msg: Prover.Protocol_Output): Boolean =
       msg.properties match {
         case Markup.Simp_Trace_Cancel(serial) =>
@@ -299,12 +305,6 @@
           false
       }
 
-    override def exit() =
-    {
-      manager.send(Clear_Memory)
-      manager.shutdown()
-    }
-
     val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel _)
   }
 }