src/Pure/PIDE/batch_session.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64115 68619fa37ca7
child 65206 ff8c3c29a924
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/PIDE/batch_session.scala
     2     Author:     Makarius
     3 
     4 PIDE session in batch mode.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import isabelle._
    11 
    12 
    13 object Batch_Session
    14 {
    15   def batch_session(
    16     options: Options,
    17     verbose: Boolean = false,
    18     dirs: List[Path] = Nil,
    19     session: String): Batch_Session =
    20   {
    21     val (_, session_tree) = Sessions.load(options, dirs).selection(sessions = List(session))
    22     val session_info = session_tree(session)
    23     val parent_session =
    24       session_info.parent getOrElse error("No parent session for " + quote(session))
    25 
    26     if (!Build.build(options, new Console_Progress(verbose = verbose),
    27         verbose = verbose, build_heap = true,
    28         dirs = dirs, sessions = List(parent_session)).ok)
    29       new RuntimeException
    30 
    31     val deps = Build.dependencies(verbose = verbose, tree = session_tree)
    32     val resources = new Resources(deps(parent_session))
    33 
    34     val progress = new Console_Progress(verbose = verbose)
    35 
    36     val prover_session = new Session(resources)
    37     val batch_session = new Batch_Session(prover_session)
    38 
    39     val handler = new Build.Handler(progress, session)
    40 
    41     prover_session.phase_changed +=
    42       Session.Consumer[Session.Phase](getClass.getName) {
    43         case Session.Ready =>
    44           prover_session.add_protocol_handler(handler)
    45           val master_dir = session_info.dir
    46           val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
    47           batch_session.build_theories_result =
    48             Some(Build.build_theories(prover_session, master_dir, theories))
    49         case Session.Inactive | Session.Failed =>
    50           batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
    51         case Session.Shutdown =>
    52           batch_session.session_result.fulfill(())
    53         case _ =>
    54       }
    55 
    56     prover_session.start(receiver =>
    57       Isabelle_Process(options, logic = parent_session, receiver = receiver))
    58 
    59     batch_session
    60   }
    61 }
    62 
    63 class Batch_Session private(val session: Session)
    64 {
    65   val session_result = Future.promise[Unit]
    66   @volatile var build_theories_result: Option[Promise[XML.Body]] = None
    67 }
    68