src/Pure/PIDE/batch_session.scala

clarified build_theories;

/*  Title:      Pure/Tools/batch_session.scala
    Author:     Makarius

PIDE session in batch mode.
*/

package isabelle


import isabelle._


object Batch_Session
{
  def batch_session(
    options: Options,
    verbose: Boolean = false,
    dirs: List[Path] = Nil,
    session: String)
  {
    val (_, session_tree) =
      Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
    val session_info = session_tree(session)
    val parent_session =
      session_info.parent getOrElse error("No parent session for " + quote(session))

    if (Build.build(options, new Build.Console_Progress(verbose),
        verbose = verbose, build_heap = true,
        dirs = dirs, sessions = List(parent_session)) != 0)
      new RuntimeException

    val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
    val resources =
    {
      val content = deps(parent_session)
      new Resources(content.loaded_theories, content.known_theories, content.syntax)
    }

    val progress = new Build.Console_Progress(verbose)
    val result = Future.promise[Unit]

    val prover_session = new Session(resources)

    prover_session.phase_changed +=
      Session.Consumer[Session.Phase](getClass.getName) {
        case Session.Ready =>
          val id = Document_ID.make().toString
          val master_dir = session_info.dir
          val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
          prover_session.build_theories(id, master_dir, theories)
          // FIXME proper check of result!?
        case Session.Inactive | Session.Failed =>
          result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
        case Session.Shutdown =>
          result.fulfill(())
        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))

    result.join
  }
}