# 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 _) } }