author | wenzelm |
Wed, 14 Jan 2015 17:24:55 +0100 | |
changeset 59367 | 6193bbbbe564 |
parent 59366 | e94df7f6b608 |
child 59369 | 7090199d3f78 |
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, |
|
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
19 |
session: String): Boolean = |
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 |
|
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
41 |
val session_result = Future.promise[Unit] |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
42 |
@volatile var build_theories_result: Option[Promise[Boolean]] = None |
59362 | 43 |
|
44 |
val prover_session = new Session(resources) |
|
45 |
||
59367 | 46 |
val handler = new Build.Handler(progress, session) |
47 |
||
59362 | 48 |
prover_session.phase_changed += |
49 |
Session.Consumer[Session.Phase](getClass.getName) { |
|
50 |
case Session.Ready => |
|
59367 | 51 |
prover_session.add_protocol_handler(handler) |
59362 | 52 |
val master_dir = session_info.dir |
59364 | 53 |
val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) }) |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
54 |
build_theories_result = |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
55 |
Some(Build.build_theories(prover_session, master_dir, theories)) |
59362 | 56 |
case Session.Inactive | Session.Failed => |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
57 |
session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated"))) |
59362 | 58 |
case Session.Shutdown => |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
59 |
session_result.fulfill(()) |
59362 | 60 |
case _ => |
61 |
} |
|
62 |
||
63 |
prover_session.start("Isabelle", List("-r", "-q", parent_session)) |
|
64 |
||
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
65 |
session_result.join |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
66 |
build_theories_result match { |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
67 |
case None => false |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
68 |
case Some(promise) => promise.join |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
69 |
} |
59362 | 70 |
} |
71 |
} |
|
72 |