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) = Sessions.load(options, dirs).selection(sessions = List(session)) |
|
22 val session_info = session_tree(session) |
|
23 val parent_session = |
|
24 session_info.parent getOrElse error("No parent session for " + quote(session)) |
|
25 |
|
26 if (!Build.build(options, new Console_Progress(verbose = verbose), |
|
27 verbose = verbose, build_heap = true, |
|
28 dirs = dirs, sessions = List(parent_session)).ok) |
|
29 throw new RuntimeException |
|
30 |
|
31 val deps = Sessions.dependencies(verbose = verbose, tree = session_tree) |
|
32 val resources = new Resources(deps(parent_session)) |
|
33 |
|
34 val progress = new Console_Progress(verbose = verbose) |
|
35 |
|
36 val prover_session = new Session(options, resources) |
|
37 val batch_session = new Batch_Session(prover_session) |
|
38 |
|
39 val handler = new Build.Handler(progress, session) |
|
40 |
|
41 Isabelle_Process.start(prover_session, options, logic = parent_session, |
|
42 phase_changed = |
|
43 { |
|
44 case Session.Ready => |
|
45 prover_session.add_protocol_handler(handler) |
|
46 val master_dir = session_info.dir |
|
47 val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) }) |
|
48 batch_session.build_theories_result = |
|
49 Some(Build.build_theories(prover_session, master_dir, theories)) |
|
50 case Session.Terminated(rc) => |
|
51 batch_session.session_result.fulfill(rc) |
|
52 case _ => |
|
53 }) |
|
54 |
|
55 batch_session |
|
56 } |
|
57 } |
|
58 |
|
59 class Batch_Session private(val session: Session) |
|
60 { |
|
61 val session_result = Future.promise[Int] |
|
62 @volatile var build_theories_result: Option[Promise[XML.Body]] = None |
|
63 } |
|
64 |
|