|
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, |
|
19 session: String) |
|
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) |
|
40 val result = Future.promise[Unit] |
|
41 |
|
42 val prover_session = new Session(resources) |
|
43 |
|
44 prover_session.phase_changed += |
|
45 Session.Consumer[Session.Phase](getClass.getName) { |
|
46 case Session.Ready => |
|
47 val master_dir = session_info.dir |
|
48 for ((_, thy_options, thy_files) <- session_info.theories) { |
|
49 val id = Document_ID.make().toString |
|
50 prover_session.use_theories(options, id, master_dir, thy_files) // FIXME proper check of result!? |
|
51 } |
|
52 case Session.Inactive | Session.Failed => |
|
53 result.fulfill_result(Exn.Exn(ERROR("Prover process terminated"))) |
|
54 case Session.Shutdown => |
|
55 result.fulfill(()) |
|
56 case _ => |
|
57 } |
|
58 |
|
59 prover_session.all_messages += |
|
60 Session.Consumer[Prover.Message](getClass.getName) { |
|
61 case msg: Prover.Output => |
|
62 msg.properties match { |
|
63 case Markup.Loading_Theory(name) => progress.theory(session, name) |
|
64 case _ => |
|
65 } |
|
66 case _ => |
|
67 } |
|
68 |
|
69 prover_session.start("Isabelle", List("-r", "-q", parent_session)) |
|
70 |
|
71 result.join |
|
72 } |
|
73 } |
|
74 |