tuned;
authorwenzelm
Tue Mar 14 00:13:38 2017 +0100 (2017-03-14)
changeset 65220420f55912b3e
parent 65219 ed4b47b8c7dc
child 65221 6af51a47545b
tuned;
src/Pure/System/invoke_scala.scala
src/Pure/Tools/build.scala
src/Pure/Tools/print_operation.scala
src/Pure/Tools/simplifier_trace.scala
     1.1 --- a/src/Pure/System/invoke_scala.scala	Tue Mar 14 00:09:15 2017 +0100
     1.2 +++ b/src/Pure/System/invoke_scala.scala	Tue Mar 14 00:13:38 2017 +0100
     1.3 @@ -77,6 +77,12 @@
     1.4    override def init(init_session: Session): Unit =
     1.5      synchronized { session = init_session }
     1.6  
     1.7 +  override def exit(): Unit = synchronized
     1.8 +  {
     1.9 +    for ((id, future) <- futures) cancel(id, future)
    1.10 +    futures = Map.empty
    1.11 +  }
    1.12 +
    1.13    private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
    1.14      synchronized
    1.15      {
    1.16 @@ -119,12 +125,6 @@
    1.17      }
    1.18    }
    1.19  
    1.20 -  override def exit(): Unit = synchronized
    1.21 -  {
    1.22 -    for ((id, future) <- futures) cancel(id, future)
    1.23 -    futures = Map.empty
    1.24 -  }
    1.25 -
    1.26    val functions =
    1.27      List(
    1.28        Markup.INVOKE_SCALA -> invoke_scala _,
     2.1 --- a/src/Pure/Tools/build.scala	Tue Mar 14 00:09:15 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 14 00:13:38 2017 +0100
     2.3 @@ -806,6 +806,9 @@
     2.4    {
     2.5      private val pending = Synchronized(Map.empty[String, Promise[XML.Body]])
     2.6  
     2.7 +    override def exit(): Unit =
     2.8 +      pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
     2.9 +
    2.10      def build_theories(
    2.11        session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
    2.12      {
    2.13 @@ -839,9 +842,6 @@
    2.14          case _ => false
    2.15        }
    2.16  
    2.17 -    override def exit(): Unit =
    2.18 -      pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
    2.19 -
    2.20      val functions =
    2.21        List(
    2.22          Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
     3.1 --- a/src/Pure/Tools/print_operation.scala	Tue Mar 14 00:09:15 2017 +0100
     3.2 +++ b/src/Pure/Tools/print_operation.scala	Tue Mar 14 00:13:38 2017 +0100
     3.3 @@ -22,6 +22,9 @@
     3.4    {
     3.5      private val print_operations = Synchronized[List[(String, String)]](Nil)
     3.6  
     3.7 +    override def init(session: Session): Unit =
     3.8 +      session.protocol_command(Markup.PRINT_OPERATIONS)
     3.9 +
    3.10      def get: List[(String, String)] = print_operations.value
    3.11  
    3.12      private def put(msg: Prover.Protocol_Output): Boolean =
    3.13 @@ -35,9 +38,6 @@
    3.14        true
    3.15      }
    3.16  
    3.17 -    override def init(session: Session): Unit =
    3.18 -      session.protocol_command(Markup.PRINT_OPERATIONS)
    3.19 -
    3.20      val functions = List(Markup.PRINT_OPERATIONS -> put _)
    3.21    }
    3.22  }
     4.1 --- a/src/Pure/Tools/simplifier_trace.scala	Tue Mar 14 00:09:15 2017 +0100
     4.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Tue Mar 14 00:13:38 2017 +0100
     4.3 @@ -290,6 +290,12 @@
     4.4    {
     4.5      assert(manager.is_active)
     4.6  
     4.7 +    override def exit() =
     4.8 +    {
     4.9 +      manager.send(Clear_Memory)
    4.10 +      manager.shutdown()
    4.11 +    }
    4.12 +
    4.13      private def cancel(msg: Prover.Protocol_Output): Boolean =
    4.14        msg.properties match {
    4.15          case Markup.Simp_Trace_Cancel(serial) =>
    4.16 @@ -299,12 +305,6 @@
    4.17            false
    4.18        }
    4.19  
    4.20 -    override def exit() =
    4.21 -    {
    4.22 -      manager.send(Clear_Memory)
    4.23 -      manager.shutdown()
    4.24 -    }
    4.25 -
    4.26      val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel _)
    4.27    }
    4.28  }