src/Pure/Tools/build.scala
changeset 59367 6193bbbbe564
parent 59366 e94df7f6b608
child 59369 7090199d3f78
     1.1 --- a/src/Pure/Tools/build.scala	Wed Jan 14 16:27:19 2015 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Jan 14 17:24:55 2015 +0100
     1.3 @@ -1029,16 +1029,14 @@
     1.4  
     1.5    /* PIDE protocol */
     1.6  
     1.7 -  val handler_name = "isabelle.Build$Handler"
     1.8 -
     1.9    def build_theories(
    1.10      session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
    1.11 -      session.get_protocol_handler(handler_name) match {
    1.12 +      session.get_protocol_handler(classOf[Handler].getName) match {
    1.13          case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
    1.14          case _ => error("Cannot invoke build_theories: bad protocol handler")
    1.15        }
    1.16  
    1.17 -  class Handler extends Session.Protocol_Handler
    1.18 +  class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler
    1.19    {
    1.20      private val pending = Synchronized(Map.empty[String, Promise[Boolean]])
    1.21  
    1.22 @@ -1052,6 +1050,12 @@
    1.23        promise
    1.24      }
    1.25  
    1.26 +    private def loading_theory(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    1.27 +      msg.properties match {
    1.28 +        case Markup.Loading_Theory(name) => progress.theory(session_name, name); true
    1.29 +        case _ => false
    1.30 +      }
    1.31 +
    1.32      private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    1.33        msg.properties match {
    1.34          case Markup.Build_Theories_Result(id, ok) =>
    1.35 @@ -1066,7 +1070,10 @@
    1.36      override def stop(prover: Prover): Unit =
    1.37        pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
    1.38  
    1.39 -    val functions = Map(Markup.BUILD_THEORIES_RESULT -> build_theories_result _)
    1.40 +    val functions =
    1.41 +      Map(
    1.42 +        Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
    1.43 +        Markup.LOADING_THEORY -> loading_theory _)
    1.44    }
    1.45  }
    1.46