author | wenzelm |
Mon, 24 Oct 2016 15:00:13 +0200 | |
changeset 64375 | 74a2af7c5145 |
parent 64115 | 68619fa37ca7 |
child 64854 | f5aa712e6250 |
permissions | -rw-r--r-- |
59720 | 1 |
/* Title: Pure/PIDE/batch_session.scala |
59362 | 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 |
{ |
62635 | 21 |
val (_, session_tree) = Sessions.load(options, dirs).selection(sessions = List(session)) |
59362 | 22 |
val session_info = session_tree(session) |
23 |
val parent_session = |
|
24 |
session_info.parent getOrElse error("No parent session for " + quote(session)) |
|
25 |
||
64115 | 26 |
if (!Build.build(options, new Console_Progress(verbose = verbose), |
59362 | 27 |
verbose = verbose, build_heap = true, |
62641 | 28 |
dirs = dirs, sessions = List(parent_session)).ok) |
59362 | 29 |
new RuntimeException |
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 | 32 |
val resources = |
33 |
{ |
|
34 |
val content = deps(parent_session) |
|
35 |
new Resources(content.loaded_theories, content.known_theories, content.syntax) |
|
36 |
} |
|
37 |
||
64115 | 38 |
val progress = new Console_Progress(verbose = verbose) |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
39 |
|
59362 | 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 | 42 |
|
59367 | 43 |
val handler = new Build.Handler(progress, session) |
44 |
||
59362 | 45 |
prover_session.phase_changed += |
46 |
Session.Consumer[Session.Phase](getClass.getName) { |
|
47 |
case Session.Ready => |
|
59367 | 48 |
prover_session.add_protocol_handler(handler) |
59362 | 49 |
val master_dir = session_info.dir |
59364 | 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 | 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 | 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 | 57 |
case _ => |
58 |
} |
|
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 | 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 |