src/Pure/PIDE/batch_session.scala
author wenzelm
Wed Apr 01 15:41:08 2015 +0200 (2015-04-01)
changeset 59891 9ce697050455
parent 59720 f893472fff31
child 59892 2a616319c171
permissions -rw-r--r--
added isabelle build option -k, for fast off-line checking of theory sources;
     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) =
    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(verbose = verbose, tree = 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 prover_session = new Session(resources)
    42     val batch_session = new Batch_Session(prover_session)
    43 
    44     val handler = new Build.Handler(progress, session)
    45 
    46     prover_session.phase_changed +=
    47       Session.Consumer[Session.Phase](getClass.getName) {
    48         case Session.Ready =>
    49           prover_session.add_protocol_handler(handler)
    50           val master_dir = session_info.dir
    51           val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
    52           batch_session.build_theories_result =
    53             Some(Build.build_theories(prover_session, master_dir, theories))
    54         case Session.Inactive | Session.Failed =>
    55           batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
    56         case Session.Shutdown =>
    57           batch_session.session_result.fulfill(())
    58         case _ =>
    59       }
    60 
    61     prover_session.start("Isabelle", List("-r", "-q", parent_session))
    62 
    63     batch_session
    64   }
    65 }
    66 
    67 class Batch_Session private(val session: Session)
    68 {
    69   val session_result = Future.promise[Unit]
    70   @volatile var build_theories_result: Option[Promise[XML.Body]] = None
    71 }
    72