src/Pure/PIDE/batch_session.scala
author wenzelm
Wed Jan 14 17:24:55 2015 +0100 (2015-01-14 ago)
changeset 59367 6193bbbbe564
parent 59366 e94df7f6b608
child 59369 7090199d3f78
permissions -rw-r--r--
more type-safe handler interface;
proper progress for Build.Handler;
     1 /*  Title:      Pure/Tools/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): Boolean =
    20   {
    21     val (_, session_tree) =
    22       Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
    23     val session_info = session_tree(session)
    24     val parent_session =
    25       session_info.parent getOrElse error("No parent session for " + quote(session))
    26 
    27     if (Build.build(options, new Build.Console_Progress(verbose),
    28         verbose = verbose, build_heap = true,
    29         dirs = dirs, sessions = List(parent_session)) != 0)
    30       new RuntimeException
    31 
    32     val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
    33     val resources =
    34     {
    35       val content = deps(parent_session)
    36       new Resources(content.loaded_theories, content.known_theories, content.syntax)
    37     }
    38 
    39     val progress = new Build.Console_Progress(verbose)
    40 
    41     val session_result = Future.promise[Unit]
    42     @volatile var build_theories_result: Option[Promise[Boolean]] = None
    43 
    44     val prover_session = new Session(resources)
    45 
    46     val handler = new Build.Handler(progress, session)
    47 
    48     prover_session.phase_changed +=
    49       Session.Consumer[Session.Phase](getClass.getName) {
    50         case Session.Ready =>
    51           prover_session.add_protocol_handler(handler)
    52           val master_dir = session_info.dir
    53           val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
    54           build_theories_result =
    55             Some(Build.build_theories(prover_session, master_dir, theories))
    56         case Session.Inactive | Session.Failed =>
    57           session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
    58         case Session.Shutdown =>
    59           session_result.fulfill(())
    60         case _ =>
    61       }
    62 
    63     prover_session.start("Isabelle", List("-r", "-q", parent_session))
    64 
    65     session_result.join
    66     build_theories_result match {
    67       case None => false
    68       case Some(promise) => promise.join
    69     }
    70   }
    71 }
    72