src/Pure/Tools/build.scala
changeset 59366 e94df7f6b608
parent 59319 677615cba30d
child 59367 6193bbbbe564
     1.1 --- a/src/Pure/Tools/build.scala	Wed Jan 14 16:23:33 2015 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Jan 14 16:27:19 2015 +0100
     1.3 @@ -1025,5 +1025,48 @@
     1.4        }
     1.5      }
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* PIDE protocol */
    1.10 +
    1.11 +  val handler_name = "isabelle.Build$Handler"
    1.12 +
    1.13 +  def build_theories(
    1.14 +    session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
    1.15 +      session.get_protocol_handler(handler_name) match {
    1.16 +        case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
    1.17 +        case _ => error("Cannot invoke build_theories: bad protocol handler")
    1.18 +      }
    1.19 +
    1.20 +  class Handler extends Session.Protocol_Handler
    1.21 +  {
    1.22 +    private val pending = Synchronized(Map.empty[String, Promise[Boolean]])
    1.23 +
    1.24 +    def build_theories(
    1.25 +      session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
    1.26 +    {
    1.27 +      val promise = Future.promise[Boolean]
    1.28 +      val id = Document_ID.make().toString
    1.29 +      pending.change(promises => promises + (id -> promise))
    1.30 +      session.build_theories(id, master_dir, theories)
    1.31 +      promise
    1.32 +    }
    1.33 +
    1.34 +    private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    1.35 +      msg.properties match {
    1.36 +        case Markup.Build_Theories_Result(id, ok) =>
    1.37 +          pending.change_result(promises =>
    1.38 +            promises.get(id) match {
    1.39 +              case Some(promise) => promise.fulfill(ok); (true, promises - id)
    1.40 +              case None => (false, promises)
    1.41 +            })
    1.42 +        case _ => false
    1.43 +      }
    1.44 +
    1.45 +    override def stop(prover: Prover): Unit =
    1.46 +      pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
    1.47 +
    1.48 +    val functions = Map(Markup.BUILD_THEORIES_RESULT -> build_theories_result _)
    1.49 +  }
    1.50  }
    1.51