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