src/Pure/PIDE/batch_session.scala
author wenzelm
Mon, 24 Oct 2016 15:00:13 +0200
changeset 64375 74a2af7c5145
parent 64115 68619fa37ca7
child 64854 f5aa712e6250
permissions -rw-r--r--
remove old target: it is on the classpath and may break scalac;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59720
f893472fff31 proper headers;
wenzelm
parents: 59369
diff changeset
     1
/*  Title:      Pure/PIDE/batch_session.scala
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
     3
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
     4
PIDE session in batch mode.
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
     5
*/
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
     6
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
     7
package isabelle
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
     8
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
     9
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    10
import isabelle._
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    11
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    12
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    13
object Batch_Session
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    14
{
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    15
  def batch_session(
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    16
    options: Options,
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    17
    verbose: Boolean = false,
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    18
    dirs: List[Path] = Nil,
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    19
    session: String): Batch_Session =
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    20
  {
62635
4854a38061de tuned signature;
wenzelm
parents: 62634
diff changeset
    21
    val (_, session_tree) = Sessions.load(options, dirs).selection(sessions = List(session))
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    22
    val session_info = session_tree(session)
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    23
    val parent_session =
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    24
      session_info.parent getOrElse error("No parent session for " + quote(session))
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    25
64115
wenzelm
parents: 62641
diff changeset
    26
    if (!Build.build(options, new Console_Progress(verbose = verbose),
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    27
        verbose = verbose, build_heap = true,
62641
0b1b7465f2ef always build with full results;
wenzelm
parents: 62635
diff changeset
    28
        dirs = dirs, sessions = List(parent_session)).ok)
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    29
      new RuntimeException
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    30
59891
9ce697050455 added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents: 59720
diff changeset
    31
    val deps = Build.dependencies(verbose = verbose, tree = session_tree)
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    32
    val resources =
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    33
    {
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    34
      val content = deps(parent_session)
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    35
      new Resources(content.loaded_theories, content.known_theories, content.syntax)
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    36
    }
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    37
64115
wenzelm
parents: 62641
diff changeset
    38
    val progress = new Console_Progress(verbose = verbose)
59366
e94df7f6b608 clarified build_theories: proper protocol handler;
wenzelm
parents: 59364
diff changeset
    39
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    40
    val prover_session = new Session(resources)
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    41
    val batch_session = new Batch_Session(prover_session)
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    42
59367
6193bbbbe564 more type-safe handler interface;
wenzelm
parents: 59366
diff changeset
    43
    val handler = new Build.Handler(progress, session)
6193bbbbe564 more type-safe handler interface;
wenzelm
parents: 59366
diff changeset
    44
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    45
    prover_session.phase_changed +=
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    46
      Session.Consumer[Session.Phase](getClass.getName) {
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    47
        case Session.Ready =>
59367
6193bbbbe564 more type-safe handler interface;
wenzelm
parents: 59366
diff changeset
    48
          prover_session.add_protocol_handler(handler)
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    49
          val master_dir = session_info.dir
59364
3b5da177ae6b clarified build_theories;
wenzelm
parents: 59362
diff changeset
    50
          val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    51
          batch_session.build_theories_result =
59366
e94df7f6b608 clarified build_theories: proper protocol handler;
wenzelm
parents: 59364
diff changeset
    52
            Some(Build.build_theories(prover_session, master_dir, theories))
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    53
        case Session.Inactive | Session.Failed =>
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    54
          batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    55
        case Session.Shutdown =>
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    56
          batch_session.session_result.fulfill(())
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    57
        case _ =>
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    58
      }
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    59
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62545
diff changeset
    60
    prover_session.start(receiver =>
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62631
diff changeset
    61
      Isabelle_Process(options, logic = parent_session, receiver = receiver))
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    62
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    63
    batch_session
59362
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    64
  }
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    65
}
41f1645a4f63 some support for PIDE batch session;
wenzelm
parents:
diff changeset
    66
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    67
class Batch_Session private(val session: Session)
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    68
{
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    69
  val session_result = Future.promise[Unit]
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    70
  @volatile var build_theories_result: Option[Promise[XML.Body]] = None
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    71
}
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59367
diff changeset
    72