more type-safe handler interface;
authorwenzelm
Wed Jan 14 17:24:55 2015 +0100 (2015-01-14)
changeset 593676193bbbbe564
parent 59366 e94df7f6b608
child 59368 100db5cf5be5
more type-safe handler interface;
proper progress for Build.Handler;
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/markup.scala
src/Pure/PIDE/session.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Wed Jan 14 16:27:19 2015 +0100
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Wed Jan 14 17:24:55 2015 +0100
     1.3 @@ -43,10 +43,12 @@
     1.4  
     1.5      val prover_session = new Session(resources)
     1.6  
     1.7 +    val handler = new Build.Handler(progress, session)
     1.8 +
     1.9      prover_session.phase_changed +=
    1.10        Session.Consumer[Session.Phase](getClass.getName) {
    1.11          case Session.Ready =>
    1.12 -          prover_session.add_protocol_handler(Build.handler_name)
    1.13 +          prover_session.add_protocol_handler(handler)
    1.14            val master_dir = session_info.dir
    1.15            val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
    1.16            build_theories_result =
    1.17 @@ -58,16 +60,6 @@
    1.18          case _ =>
    1.19        }
    1.20  
    1.21 -    prover_session.all_messages +=
    1.22 -      Session.Consumer[Prover.Message](getClass.getName) {
    1.23 -        case msg: Prover.Output =>
    1.24 -          msg.properties match {
    1.25 -            case Markup.Loading_Theory(name) => progress.theory(session, name)
    1.26 -            case _ =>
    1.27 -          }
    1.28 -        case _ =>
    1.29 -      }
    1.30 -
    1.31      prover_session.start("Isabelle", List("-r", "-q", parent_session))
    1.32  
    1.33      session_result.join
     2.1 --- a/src/Pure/PIDE/markup.scala	Wed Jan 14 16:27:19 2015 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jan 14 17:24:55 2015 +0100
     2.3 @@ -458,11 +458,12 @@
     2.4        }
     2.5    }
     2.6  
     2.7 +  val LOADING_THEORY = "loading_theory"
     2.8    object Loading_Theory
     2.9    {
    2.10      def unapply(props: Properties.T): Option[String] =
    2.11        props match {
    2.12 -        case List((FUNCTION, "loading_theory"), (NAME, name)) => Some(name)
    2.13 +        case List((FUNCTION, LOADING_THEORY), (NAME, name)) => Some(name)
    2.14          case _ => None
    2.15        }
    2.16    }
     3.1 --- a/src/Pure/PIDE/session.scala	Wed Jan 14 16:27:19 2015 +0100
     3.2 +++ b/src/Pure/PIDE/session.scala	Wed Jan 14 17:24:55 2015 +0100
     3.3 @@ -105,14 +105,20 @@
     3.4      val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
     3.5    }
     3.6  
     3.7 +  def bad_protocol_handler(exn: Throwable, name: String): Unit =
     3.8 +    Output.error_message(
     3.9 +      "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
    3.10 +
    3.11    private class Protocol_Handlers(
    3.12      handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    3.13      functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
    3.14    {
    3.15      def get(name: String): Option[Protocol_Handler] = handlers.get(name)
    3.16  
    3.17 -    def add(prover: Prover, name: String): Protocol_Handlers =
    3.18 +    def add(prover: Prover, handler: Protocol_Handler): Protocol_Handlers =
    3.19      {
    3.20 +      val name = handler.getClass.getName
    3.21 +
    3.22        val (handlers1, functions1) =
    3.23          handlers.get(name) match {
    3.24            case Some(old_handler) =>
    3.25 @@ -124,22 +130,20 @@
    3.26  
    3.27        val (handlers2, functions2) =
    3.28          try {
    3.29 -          val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
    3.30 -          new_handler.start(prover)
    3.31 +          handler.start(prover)
    3.32  
    3.33            val new_functions =
    3.34 -            for ((a, f) <- new_handler.functions.toList) yield
    3.35 +            for ((a, f) <- handler.functions.toList) yield
    3.36                (a, (msg: Prover.Protocol_Output) => f(prover, msg))
    3.37  
    3.38            val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    3.39            if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    3.40  
    3.41 -          (handlers1 + (name -> new_handler), functions1 ++ new_functions)
    3.42 +          (handlers1 + (name -> handler), functions1 ++ new_functions)
    3.43          }
    3.44          catch {
    3.45            case exn: Throwable =>
    3.46 -            Output.error_message(
    3.47 -              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
    3.48 +            Session.bad_protocol_handler(exn, name)
    3.49              (handlers1, functions1)
    3.50          }
    3.51  
    3.52 @@ -342,8 +346,8 @@
    3.53    def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
    3.54      _protocol_handlers.value.get(name)
    3.55  
    3.56 -  def add_protocol_handler(name: String): Unit =
    3.57 -    _protocol_handlers.change(_.add(prover.get, name))
    3.58 +  def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
    3.59 +    _protocol_handlers.change(_.add(prover.get, handler))
    3.60  
    3.61  
    3.62    /* manager thread */
    3.63 @@ -439,7 +443,12 @@
    3.64            if (!handled) {
    3.65              msg.properties match {
    3.66                case Markup.Protocol_Handler(name) if prover.defined =>
    3.67 -                add_protocol_handler(name)
    3.68 +                try {
    3.69 +                  val handler =
    3.70 +                    Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]
    3.71 +                  add_protocol_handler(handler)
    3.72 +                }
    3.73 +                catch { case exn: Throwable => Session.bad_protocol_handler(exn, name) }
    3.74  
    3.75                case Protocol.Command_Timing(state_id, timing) if prover.defined =>
    3.76                  val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
     4.1 --- a/src/Pure/Tools/build.scala	Wed Jan 14 16:27:19 2015 +0100
     4.2 +++ b/src/Pure/Tools/build.scala	Wed Jan 14 17:24:55 2015 +0100
     4.3 @@ -1029,16 +1029,14 @@
     4.4  
     4.5    /* PIDE protocol */
     4.6  
     4.7 -  val handler_name = "isabelle.Build$Handler"
     4.8 -
     4.9    def build_theories(
    4.10      session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
    4.11 -      session.get_protocol_handler(handler_name) match {
    4.12 +      session.get_protocol_handler(classOf[Handler].getName) match {
    4.13          case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
    4.14          case _ => error("Cannot invoke build_theories: bad protocol handler")
    4.15        }
    4.16  
    4.17 -  class Handler extends Session.Protocol_Handler
    4.18 +  class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler
    4.19    {
    4.20      private val pending = Synchronized(Map.empty[String, Promise[Boolean]])
    4.21  
    4.22 @@ -1052,6 +1050,12 @@
    4.23        promise
    4.24      }
    4.25  
    4.26 +    private def loading_theory(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    4.27 +      msg.properties match {
    4.28 +        case Markup.Loading_Theory(name) => progress.theory(session_name, name); true
    4.29 +        case _ => false
    4.30 +      }
    4.31 +
    4.32      private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    4.33        msg.properties match {
    4.34          case Markup.Build_Theories_Result(id, ok) =>
    4.35 @@ -1066,7 +1070,10 @@
    4.36      override def stop(prover: Prover): Unit =
    4.37        pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
    4.38  
    4.39 -    val functions = Map(Markup.BUILD_THEORIES_RESULT -> build_theories_result _)
    4.40 +    val functions =
    4.41 +      Map(
    4.42 +        Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
    4.43 +        Markup.LOADING_THEORY -> loading_theory _)
    4.44    }
    4.45  }
    4.46