author | wenzelm |
Thu, 15 Jan 2015 12:54:08 +0100 | |
changeset 59369 | 7090199d3f78 |
parent 59367 | 6193bbbbe564 |
child 59720 | f893472fff31 |
permissions | -rw-r--r-- |
59362 | 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, |
|
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
19 |
session: String): Batch_Session = |
59362 | 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) |
|
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
40 |
|
59362 | 41 |
val prover_session = new Session(resources) |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
42 |
val batch_session = new Batch_Session(prover_session) |
59362 | 43 |
|
59367 | 44 |
val handler = new Build.Handler(progress, session) |
45 |
||
59362 | 46 |
prover_session.phase_changed += |
47 |
Session.Consumer[Session.Phase](getClass.getName) { |
|
48 |
case Session.Ready => |
|
59367 | 49 |
prover_session.add_protocol_handler(handler) |
59362 | 50 |
val master_dir = session_info.dir |
59364 | 51 |
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
|
52 |
batch_session.build_theories_result = |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
53 |
Some(Build.build_theories(prover_session, master_dir, theories)) |
59362 | 54 |
case Session.Inactive | Session.Failed => |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
55 |
batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated"))) |
59362 | 56 |
case Session.Shutdown => |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
57 |
batch_session.session_result.fulfill(()) |
59362 | 58 |
case _ => |
59 |
} |
|
60 |
||
61 |
prover_session.start("Isabelle", List("-r", "-q", parent_session)) |
|
62 |
||
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
63 |
batch_session |
59362 | 64 |
} |
65 |
} |
|
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 |