misc tuning and simplification;
authorwenzelm
Tue Mar 14 00:09:15 2017 +0100 (2017-03-14)
changeset 65219ed4b47b8c7dc
parent 65218 102b8e092860
child 65220 420f55912b3e
misc tuning and simplification;
src/Pure/PIDE/protocol_handlers.scala
src/Pure/PIDE/session.scala
src/Pure/System/invoke_scala.scala
src/Pure/Tools/build.scala
src/Pure/Tools/debugger.scala
src/Pure/Tools/print_operation.scala
src/Pure/Tools/simplifier_trace.scala
     1.1 --- a/src/Pure/PIDE/protocol_handlers.scala	Mon Mar 13 23:24:20 2017 +0100
     1.2 +++ b/src/Pure/PIDE/protocol_handlers.scala	Tue Mar 14 00:09:15 2017 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4    {
     1.5      def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
     1.6  
     1.7 -    def add(prover: Prover, handler: Session.Protocol_Handler): State =
     1.8 +    def add(handler: Session.Protocol_Handler): State =
     1.9      {
    1.10        val name = handler.getClass.getName
    1.11  
    1.12 @@ -28,23 +28,19 @@
    1.13          handlers.get(name) match {
    1.14            case Some(old_handler) =>
    1.15              Output.warning("Redefining protocol handler: " + name)
    1.16 -            old_handler.stop(prover)
    1.17 -            (handlers - name, functions -- old_handler.functions.keys)
    1.18 +            old_handler.exit()
    1.19 +            (handlers - name, functions -- old_handler.functions.map(_._1))
    1.20            case None => (handlers, functions)
    1.21          }
    1.22  
    1.23        val (handlers2, functions2) =
    1.24          try {
    1.25 -          handler.start(session, prover)
    1.26 +          handler.init(session)
    1.27  
    1.28 -          val new_functions =
    1.29 -            for ((a, f) <- handler.functions.toList) yield
    1.30 -              (a, (msg: Prover.Protocol_Output) => f(prover, msg))
    1.31 -
    1.32 -          val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    1.33 +          val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a
    1.34            if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    1.35  
    1.36 -          (handlers1 + (name -> handler), functions1 ++ new_functions)
    1.37 +          (handlers1 + (name -> handler), functions1 ++ handler.functions)
    1.38          }
    1.39          catch {
    1.40            case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
    1.41 @@ -52,15 +48,12 @@
    1.42        copy(handlers = handlers2, functions = functions2)
    1.43      }
    1.44  
    1.45 -    def add(prover: Prover, name: String): State =
    1.46 +    def add(name: String): State =
    1.47      {
    1.48        val new_handler =
    1.49          try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
    1.50          catch { case exn: Throwable => bad_handler(exn, name); None }
    1.51 -      new_handler match {
    1.52 -        case Some(handler) => add(prover, handler)
    1.53 -        case None => this
    1.54 -      }
    1.55 +      new_handler match { case Some(handler) => add(handler) case None => this }
    1.56      }
    1.57  
    1.58      def invoke(msg: Prover.Protocol_Output): Boolean =
    1.59 @@ -76,9 +69,9 @@
    1.60          case _ => false
    1.61        }
    1.62  
    1.63 -    def stop(prover: Prover): State =
    1.64 +    def exit(): State =
    1.65      {
    1.66 -      for ((_, handler) <- handlers) handler.stop(prover)
    1.67 +      for ((_, handler) <- handlers) handler.exit()
    1.68        copy(handlers = Map.empty, functions = Map.empty)
    1.69      }
    1.70    }
    1.71 @@ -91,18 +84,9 @@
    1.72  {
    1.73    private val state = Synchronized(Protocol_Handlers.State(session))
    1.74  
    1.75 -  def get(name: String): Option[Session.Protocol_Handler] =
    1.76 -    state.value.get(name)
    1.77 -
    1.78 -  def add(prover: Prover, handler: Session.Protocol_Handler): Unit =
    1.79 -    state.change(_.add(prover, handler))
    1.80 -
    1.81 -  def add(prover: Prover, name: String): Unit =
    1.82 -    state.change(_.add(prover, name))
    1.83 -
    1.84 -  def invoke(msg: Prover.Protocol_Output): Boolean =
    1.85 -    state.value.invoke(msg)
    1.86 -
    1.87 -  def stop(prover: Prover): Unit =
    1.88 -    state.change(_.stop(prover))
    1.89 +  def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
    1.90 +  def add(handler: Session.Protocol_Handler): Unit = state.change(_.add(handler))
    1.91 +  def add(name: String): Unit = state.change(_.add(name))
    1.92 +  def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg)
    1.93 +  def exit(): Unit = state.change(_.exit())
    1.94  }
     2.1 --- a/src/Pure/PIDE/session.scala	Mon Mar 13 23:24:20 2017 +0100
     2.2 +++ b/src/Pure/PIDE/session.scala	Tue Mar 14 00:09:15 2017 +0100
     2.3 @@ -107,9 +107,9 @@
     2.4  
     2.5    abstract class Protocol_Handler
     2.6    {
     2.7 -    def start(session: Session, prover: Prover): Unit = {}
     2.8 -    def stop(prover: Prover): Unit = {}
     2.9 -    val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
    2.10 +    def init(session: Session): Unit = {}
    2.11 +    def exit(): Unit = {}
    2.12 +    val functions: List[(String, Prover.Protocol_Output => Boolean)]
    2.13    }
    2.14  }
    2.15  
    2.16 @@ -289,10 +289,10 @@
    2.17      protocol_handlers.get(name)
    2.18  
    2.19    def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
    2.20 -    protocol_handlers.add(prover.get, handler)
    2.21 +    protocol_handlers.add(handler)
    2.22  
    2.23    def add_protocol_handler(name: String): Unit =
    2.24 -    protocol_handlers.add(prover.get, name)
    2.25 +    protocol_handlers.add(name)
    2.26  
    2.27  
    2.28    /* manager thread */
    2.29 @@ -476,7 +476,7 @@
    2.30            case Stop =>
    2.31              delay_prune.revoke()
    2.32              if (prover.defined) {
    2.33 -              protocol_handlers.stop(prover.get)
    2.34 +              protocol_handlers.exit()
    2.35                global_state.change(_ => Document.State.init)
    2.36                prover.get.terminate
    2.37              }
     3.1 --- a/src/Pure/System/invoke_scala.scala	Mon Mar 13 23:24:20 2017 +0100
     3.2 +++ b/src/Pure/System/invoke_scala.scala	Tue Mar 14 00:09:15 2017 +0100
     3.3 @@ -71,43 +71,47 @@
     3.4  
     3.5  class Invoke_Scala extends Session.Protocol_Handler
     3.6  {
     3.7 +  private var session: Session = null
     3.8    private var futures = Map.empty[String, Future[Unit]]
     3.9  
    3.10 -  private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
    3.11 +  override def init(init_session: Session): Unit =
    3.12 +    synchronized { session = init_session }
    3.13 +
    3.14 +  private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
    3.15      synchronized
    3.16      {
    3.17        if (futures.isDefinedAt(id)) {
    3.18 -        prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
    3.19 +        session.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
    3.20          futures -= id
    3.21        }
    3.22      }
    3.23  
    3.24 -  private def cancel(prover: Prover, id: String, future: Future[Unit])
    3.25 +  private def cancel(id: String, future: Future[Unit])
    3.26    {
    3.27      future.cancel
    3.28 -    fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
    3.29 +    fulfill(id, Invoke_Scala.Tag.INTERRUPT, "")
    3.30    }
    3.31  
    3.32 -  private def invoke_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
    3.33 +  private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
    3.34    {
    3.35      msg.properties match {
    3.36        case Markup.Invoke_Scala(name, id) =>
    3.37          futures += (id ->
    3.38            Future.fork {
    3.39              val (tag, result) = Invoke_Scala.method(name, msg.text)
    3.40 -            fulfill(prover, id, tag, result)
    3.41 +            fulfill(id, tag, result)
    3.42            })
    3.43          true
    3.44        case _ => false
    3.45      }
    3.46    }
    3.47  
    3.48 -  private def cancel_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
    3.49 +  private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
    3.50    {
    3.51      msg.properties match {
    3.52        case Markup.Cancel_Scala(id) =>
    3.53          futures.get(id) match {
    3.54 -          case Some(future) => cancel(prover, id, future)
    3.55 +          case Some(future) => cancel(id, future)
    3.56            case None =>
    3.57          }
    3.58          true
    3.59 @@ -115,13 +119,14 @@
    3.60      }
    3.61    }
    3.62  
    3.63 -  override def stop(prover: Prover): Unit = synchronized
    3.64 +  override def exit(): Unit = synchronized
    3.65    {
    3.66 -    for ((id, future) <- futures) cancel(prover, id, future)
    3.67 +    for ((id, future) <- futures) cancel(id, future)
    3.68      futures = Map.empty
    3.69    }
    3.70  
    3.71 -  val functions = Map(
    3.72 -    Markup.INVOKE_SCALA -> invoke_scala _,
    3.73 -    Markup.CANCEL_SCALA -> cancel_scala _)
    3.74 +  val functions =
    3.75 +    List(
    3.76 +      Markup.INVOKE_SCALA -> invoke_scala _,
    3.77 +      Markup.CANCEL_SCALA -> cancel_scala _)
    3.78  }
     4.1 --- a/src/Pure/Tools/build.scala	Mon Mar 13 23:24:20 2017 +0100
     4.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 14 00:09:15 2017 +0100
     4.3 @@ -816,13 +816,13 @@
     4.4        promise
     4.5      }
     4.6  
     4.7 -    private def loading_theory(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     4.8 +    private def loading_theory(msg: Prover.Protocol_Output): Boolean =
     4.9        msg.properties match {
    4.10          case Markup.Loading_Theory(name) => progress.theory(session_name, name); true
    4.11          case _ => false
    4.12        }
    4.13  
    4.14 -    private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    4.15 +    private def build_theories_result(msg: Prover.Protocol_Output): Boolean =
    4.16        msg.properties match {
    4.17          case Markup.Build_Theories_Result(id) =>
    4.18            pending.change_result(promises =>
    4.19 @@ -839,11 +839,11 @@
    4.20          case _ => false
    4.21        }
    4.22  
    4.23 -    override def stop(prover: Prover): Unit =
    4.24 +    override def exit(): Unit =
    4.25        pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
    4.26  
    4.27      val functions =
    4.28 -      Map(
    4.29 +      List(
    4.30          Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
    4.31          Markup.LOADING_THEORY -> loading_theory _)
    4.32    }
     5.1 --- a/src/Pure/Tools/debugger.scala	Mon Mar 13 23:24:20 2017 +0100
     5.2 +++ b/src/Pure/Tools/debugger.scala	Tue Mar 14 00:09:15 2017 +0100
     5.3 @@ -120,7 +120,7 @@
     5.4      def get_debugger: Option[Debugger] = _debugger_.value
     5.5      def the_debugger: Debugger = get_debugger getOrElse error("Debugger not initialized")
     5.6  
     5.7 -    override def start(session: Session, prover: Prover)
     5.8 +    override def init(session: Session)
     5.9      {
    5.10        _debugger_.change(
    5.11          {
    5.12 @@ -129,7 +129,7 @@
    5.13          })
    5.14      }
    5.15  
    5.16 -    private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    5.17 +    private def debugger_state(msg: Prover.Protocol_Output): Boolean =
    5.18      {
    5.19        msg.properties match {
    5.20          case Markup.Debugger_State(thread_name) =>
    5.21 @@ -148,7 +148,7 @@
    5.22        }
    5.23      }
    5.24  
    5.25 -    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    5.26 +    private def debugger_output(msg: Prover.Protocol_Output): Boolean =
    5.27      {
    5.28        msg.properties match {
    5.29          case Markup.Debugger_Output(thread_name) =>
    5.30 @@ -165,7 +165,7 @@
    5.31      }
    5.32  
    5.33      val functions =
    5.34 -      Map(
    5.35 +      List(
    5.36          Markup.DEBUGGER_STATE -> debugger_state _,
    5.37          Markup.DEBUGGER_OUTPUT -> debugger_output _)
    5.38    }
     6.1 --- a/src/Pure/Tools/print_operation.scala	Mon Mar 13 23:24:20 2017 +0100
     6.2 +++ b/src/Pure/Tools/print_operation.scala	Tue Mar 14 00:09:15 2017 +0100
     6.3 @@ -24,7 +24,7 @@
     6.4  
     6.5      def get: List[(String, String)] = print_operations.value
     6.6  
     6.7 -    private def put(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     6.8 +    private def put(msg: Prover.Protocol_Output): Boolean =
     6.9      {
    6.10        val ops =
    6.11        {
    6.12 @@ -35,9 +35,9 @@
    6.13        true
    6.14      }
    6.15  
    6.16 -    override def start(session: Session, prover: Prover): Unit =
    6.17 -      prover.protocol_command(Markup.PRINT_OPERATIONS)
    6.18 +    override def init(session: Session): Unit =
    6.19 +      session.protocol_command(Markup.PRINT_OPERATIONS)
    6.20  
    6.21 -    val functions = Map(Markup.PRINT_OPERATIONS -> put _)
    6.22 +    val functions = List(Markup.PRINT_OPERATIONS -> put _)
    6.23    }
    6.24  }
     7.1 --- a/src/Pure/Tools/simplifier_trace.scala	Mon Mar 13 23:24:20 2017 +0100
     7.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Tue Mar 14 00:09:15 2017 +0100
     7.3 @@ -290,7 +290,7 @@
     7.4    {
     7.5      assert(manager.is_active)
     7.6  
     7.7 -    private def cancel(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     7.8 +    private def cancel(msg: Prover.Protocol_Output): Boolean =
     7.9        msg.properties match {
    7.10          case Markup.Simp_Trace_Cancel(serial) =>
    7.11            manager.send(Cancel(serial))
    7.12 @@ -299,12 +299,12 @@
    7.13            false
    7.14        }
    7.15  
    7.16 -    override def stop(prover: Prover) =
    7.17 +    override def exit() =
    7.18      {
    7.19        manager.send(Clear_Memory)
    7.20        manager.shutdown()
    7.21      }
    7.22  
    7.23 -    val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _)
    7.24 +    val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel _)
    7.25    }
    7.26  }