# HG changeset patch # User wenzelm # Date 1421252695 -3600 # Node ID 6193bbbbe5644b8e6957ef90a04df3d51735a070 # Parent e94df7f6b608b0648ccc0a25d394a4c35fcbfb11 more type-safe handler interface; proper progress for Build.Handler; diff -r e94df7f6b608 -r 6193bbbbe564 src/Pure/PIDE/batch_session.scala --- a/src/Pure/PIDE/batch_session.scala Wed Jan 14 16:27:19 2015 +0100 +++ b/src/Pure/PIDE/batch_session.scala Wed Jan 14 17:24:55 2015 +0100 @@ -43,10 +43,12 @@ val prover_session = new Session(resources) + val handler = new Build.Handler(progress, session) + prover_session.phase_changed += Session.Consumer[Session.Phase](getClass.getName) { case Session.Ready => - prover_session.add_protocol_handler(Build.handler_name) + prover_session.add_protocol_handler(handler) val master_dir = session_info.dir val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) }) build_theories_result = @@ -58,16 +60,6 @@ case _ => } - prover_session.all_messages += - Session.Consumer[Prover.Message](getClass.getName) { - case msg: Prover.Output => - msg.properties match { - case Markup.Loading_Theory(name) => progress.theory(session, name) - case _ => - } - case _ => - } - prover_session.start("Isabelle", List("-r", "-q", parent_session)) session_result.join diff -r e94df7f6b608 -r 6193bbbbe564 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Jan 14 16:27:19 2015 +0100 +++ b/src/Pure/PIDE/markup.scala Wed Jan 14 17:24:55 2015 +0100 @@ -458,11 +458,12 @@ } } + val LOADING_THEORY = "loading_theory" object Loading_Theory { def unapply(props: Properties.T): Option[String] = props match { - case List((FUNCTION, "loading_theory"), (NAME, name)) => Some(name) + case List((FUNCTION, LOADING_THEORY), (NAME, name)) => Some(name) case _ => None } } diff -r e94df7f6b608 -r 6193bbbbe564 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Wed Jan 14 16:27:19 2015 +0100 +++ b/src/Pure/PIDE/session.scala Wed Jan 14 17:24:55 2015 +0100 @@ -105,14 +105,20 @@ val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean] } + def bad_protocol_handler(exn: Throwable, name: String): Unit = + Output.error_message( + "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)) + private class Protocol_Handlers( handlers: Map[String, Session.Protocol_Handler] = Map.empty, functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty) { def get(name: String): Option[Protocol_Handler] = handlers.get(name) - def add(prover: Prover, name: String): Protocol_Handlers = + def add(prover: Prover, handler: Protocol_Handler): Protocol_Handlers = { + val name = handler.getClass.getName + val (handlers1, functions1) = handlers.get(name) match { case Some(old_handler) => @@ -124,22 +130,20 @@ val (handlers2, functions2) = try { - val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler] - new_handler.start(prover) + handler.start(prover) val new_functions = - for ((a, f) <- new_handler.functions.toList) yield + for ((a, f) <- handler.functions.toList) yield (a, (msg: Prover.Protocol_Output) => f(prover, msg)) val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) - (handlers1 + (name -> new_handler), functions1 ++ new_functions) + (handlers1 + (name -> handler), functions1 ++ new_functions) } catch { case exn: Throwable => - Output.error_message( - "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)) + Session.bad_protocol_handler(exn, name) (handlers1, functions1) } @@ -342,8 +346,8 @@ def get_protocol_handler(name: String): Option[Session.Protocol_Handler] = _protocol_handlers.value.get(name) - def add_protocol_handler(name: String): Unit = - _protocol_handlers.change(_.add(prover.get, name)) + def add_protocol_handler(handler: Session.Protocol_Handler): Unit = + _protocol_handlers.change(_.add(prover.get, handler)) /* manager thread */ @@ -439,7 +443,12 @@ if (!handled) { msg.properties match { case Markup.Protocol_Handler(name) if prover.defined => - add_protocol_handler(name) + try { + val handler = + Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler] + add_protocol_handler(handler) + } + catch { case exn: Throwable => Session.bad_protocol_handler(exn, name) } case Protocol.Command_Timing(state_id, timing) if prover.defined => val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) diff -r e94df7f6b608 -r 6193bbbbe564 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Jan 14 16:27:19 2015 +0100 +++ b/src/Pure/Tools/build.scala Wed Jan 14 17:24:55 2015 +0100 @@ -1029,16 +1029,14 @@ /* PIDE protocol */ - val handler_name = "isabelle.Build$Handler" - def build_theories( session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] = - session.get_protocol_handler(handler_name) match { + session.get_protocol_handler(classOf[Handler].getName) match { case Some(handler: Handler) => handler.build_theories(session, master_dir, theories) case _ => error("Cannot invoke build_theories: bad protocol handler") } - class Handler extends Session.Protocol_Handler + class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler { private val pending = Synchronized(Map.empty[String, Promise[Boolean]]) @@ -1052,6 +1050,12 @@ promise } + private def loading_theory(prover: Prover, msg: Prover.Protocol_Output): Boolean = + msg.properties match { + case Markup.Loading_Theory(name) => progress.theory(session_name, name); true + case _ => false + } + private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Build_Theories_Result(id, ok) => @@ -1066,7 +1070,10 @@ override def stop(prover: Prover): Unit = pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty }) - val functions = Map(Markup.BUILD_THEORIES_RESULT -> build_theories_result _) + val functions = + Map( + Markup.BUILD_THEORIES_RESULT -> build_theories_result _, + Markup.LOADING_THEORY -> loading_theory _) } }