src/Pure/PIDE/batch_session.scala
author wenzelm
Tue Jan 13 21:46:09 2015 +0100 (2015-01-13)
changeset 59362 41f1645a4f63
child 59364 3b5da177ae6b
permissions -rw-r--r--
some support for PIDE batch session;
clarified Thy_Info.use_thys_options and corresponding protocol command;
wenzelm@59362
     1
/*  Title:      Pure/Tools/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@59362
    19
    session: String)
wenzelm@59362
    20
  {
wenzelm@59362
    21
    val (_, session_tree) =
wenzelm@59362
    22
      Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
wenzelm@59362
    23
    val session_info = session_tree(session)
wenzelm@59362
    24
    val parent_session =
wenzelm@59362
    25
      session_info.parent getOrElse error("No parent session for " + quote(session))
wenzelm@59362
    26
wenzelm@59362
    27
    if (Build.build(options, new Build.Console_Progress(verbose),
wenzelm@59362
    28
        verbose = verbose, build_heap = true,
wenzelm@59362
    29
        dirs = dirs, sessions = List(parent_session)) != 0)
wenzelm@59362
    30
      new RuntimeException
wenzelm@59362
    31
wenzelm@59362
    32
    val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
wenzelm@59362
    33
    val resources =
wenzelm@59362
    34
    {
wenzelm@59362
    35
      val content = deps(parent_session)
wenzelm@59362
    36
      new Resources(content.loaded_theories, content.known_theories, content.syntax)
wenzelm@59362
    37
    }
wenzelm@59362
    38
wenzelm@59362
    39
    val progress = new Build.Console_Progress(verbose)
wenzelm@59362
    40
    val result = Future.promise[Unit]
wenzelm@59362
    41
wenzelm@59362
    42
    val prover_session = new Session(resources)
wenzelm@59362
    43
wenzelm@59362
    44
    prover_session.phase_changed +=
wenzelm@59362
    45
      Session.Consumer[Session.Phase](getClass.getName) {
wenzelm@59362
    46
        case Session.Ready =>
wenzelm@59362
    47
          val master_dir = session_info.dir
wenzelm@59362
    48
          for ((_, thy_options, thy_files) <- session_info.theories) {
wenzelm@59362
    49
            val id = Document_ID.make().toString
wenzelm@59362
    50
            prover_session.use_theories(options, id, master_dir, thy_files) // FIXME proper check of result!?
wenzelm@59362
    51
          }
wenzelm@59362
    52
        case Session.Inactive | Session.Failed =>
wenzelm@59362
    53
          result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
wenzelm@59362
    54
        case Session.Shutdown =>
wenzelm@59362
    55
          result.fulfill(())
wenzelm@59362
    56
        case _ =>
wenzelm@59362
    57
      }
wenzelm@59362
    58
wenzelm@59362
    59
    prover_session.all_messages +=
wenzelm@59362
    60
      Session.Consumer[Prover.Message](getClass.getName) {
wenzelm@59362
    61
        case msg: Prover.Output =>
wenzelm@59362
    62
          msg.properties match {
wenzelm@59362
    63
            case Markup.Loading_Theory(name) => progress.theory(session, name)
wenzelm@59362
    64
            case _ =>
wenzelm@59362
    65
          }
wenzelm@59362
    66
        case _ =>
wenzelm@59362
    67
      }
wenzelm@59362
    68
wenzelm@59362
    69
    prover_session.start("Isabelle", List("-r", "-q", parent_session))
wenzelm@59362
    70
wenzelm@59362
    71
    result.join
wenzelm@59362
    72
  }
wenzelm@59362
    73
}
wenzelm@59362
    74