author | wenzelm |
Mon, 13 Mar 2017 12:04:11 +0100 | |
changeset 65206 | ff8c3c29a924 |
parent 64854 | f5aa712e6250 |
child 65216 | 060a8a1f2dec |
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) |
64854 | 32 |
val resources = new Resources(deps(parent_session)) |
59362 | 33 |
|
64115 | 34 |
val progress = new Console_Progress(verbose = verbose) |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
35 |
|
59362 | 36 |
val prover_session = new Session(resources) |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
37 |
val batch_session = new Batch_Session(prover_session) |
59362 | 38 |
|
59367 | 39 |
val handler = new Build.Handler(progress, session) |
40 |
||
59362 | 41 |
prover_session.phase_changed += |
42 |
Session.Consumer[Session.Phase](getClass.getName) { |
|
43 |
case Session.Ready => |
|
59367 | 44 |
prover_session.add_protocol_handler(handler) |
59362 | 45 |
val master_dir = session_info.dir |
59364 | 46 |
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
|
47 |
batch_session.build_theories_result = |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
48 |
Some(Build.build_theories(prover_session, master_dir, theories)) |
65206 | 49 |
case Session.Terminated(_) => |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
50 |
batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated"))) |
59362 | 51 |
case Session.Shutdown => |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
52 |
batch_session.session_result.fulfill(()) |
59362 | 53 |
case _ => |
54 |
} |
|
55 |
||
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62545
diff
changeset
|
56 |
prover_session.start(receiver => |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62631
diff
changeset
|
57 |
Isabelle_Process(options, logic = parent_session, receiver = receiver)) |
59362 | 58 |
|
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
59 |
batch_session |
59362 | 60 |
} |
61 |
} |
|
62 |
||
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
63 |
class Batch_Session private(val session: Session) |
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
64 |
{ |
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
65 |
val session_result = Future.promise[Unit] |
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
66 |
@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
|
67 |
} |
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
68 |