41 val session_result = Future.promise[Unit] |
41 val session_result = Future.promise[Unit] |
42 @volatile var build_theories_result: Option[Promise[Boolean]] = None |
42 @volatile var build_theories_result: Option[Promise[Boolean]] = None |
43 |
43 |
44 val prover_session = new Session(resources) |
44 val prover_session = new Session(resources) |
45 |
45 |
|
46 val handler = new Build.Handler(progress, session) |
|
47 |
46 prover_session.phase_changed += |
48 prover_session.phase_changed += |
47 Session.Consumer[Session.Phase](getClass.getName) { |
49 Session.Consumer[Session.Phase](getClass.getName) { |
48 case Session.Ready => |
50 case Session.Ready => |
49 prover_session.add_protocol_handler(Build.handler_name) |
51 prover_session.add_protocol_handler(handler) |
50 val master_dir = session_info.dir |
52 val master_dir = session_info.dir |
51 val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) }) |
53 val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) }) |
52 build_theories_result = |
54 build_theories_result = |
53 Some(Build.build_theories(prover_session, master_dir, theories)) |
55 Some(Build.build_theories(prover_session, master_dir, theories)) |
54 case Session.Inactive | Session.Failed => |
56 case Session.Inactive | Session.Failed => |
55 session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated"))) |
57 session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated"))) |
56 case Session.Shutdown => |
58 case Session.Shutdown => |
57 session_result.fulfill(()) |
59 session_result.fulfill(()) |
58 case _ => |
|
59 } |
|
60 |
|
61 prover_session.all_messages += |
|
62 Session.Consumer[Prover.Message](getClass.getName) { |
|
63 case msg: Prover.Output => |
|
64 msg.properties match { |
|
65 case Markup.Loading_Theory(name) => progress.theory(session, name) |
|
66 case _ => |
|
67 } |
|
68 case _ => |
60 case _ => |
69 } |
61 } |
70 |
62 |
71 prover_session.start("Isabelle", List("-r", "-q", parent_session)) |
63 prover_session.start("Isabelle", List("-r", "-q", parent_session)) |
72 |
64 |