--- a/src/Pure/PIDE/batch_session.scala Sat Mar 18 20:35:58 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-/* Title: Pure/PIDE/batch_session.scala
- Author: Makarius
-
-PIDE session in batch mode.
-*/
-
-package isabelle
-
-
-import isabelle._
-
-
-object Batch_Session
-{
- def batch_session(
- options: Options,
- verbose: Boolean = false,
- dirs: List[Path] = Nil,
- session: String): Batch_Session =
- {
- val (_, session_tree) = Sessions.load(options, dirs).selection(sessions = List(session))
- val session_info = session_tree(session)
- val parent_session =
- session_info.parent getOrElse error("No parent session for " + quote(session))
-
- if (!Build.build(options, new Console_Progress(verbose = verbose),
- verbose = verbose, build_heap = true,
- dirs = dirs, sessions = List(parent_session)).ok)
- throw new RuntimeException
-
- val deps = Sessions.dependencies(verbose = verbose, tree = session_tree)
- val resources = new Resources(deps(parent_session))
-
- val progress = new Console_Progress(verbose = verbose)
-
- val prover_session = new Session(options, resources)
- val batch_session = new Batch_Session(prover_session)
-
- val handler = new Build.Handler(progress, session)
-
- Isabelle_Process.start(prover_session, options, logic = parent_session,
- phase_changed =
- {
- case Session.Ready =>
- prover_session.add_protocol_handler(handler)
- val master_dir = session_info.dir
- val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
- batch_session.build_theories_result =
- Some(Build.build_theories(prover_session, master_dir, theories))
- case Session.Terminated(rc) =>
- batch_session.session_result.fulfill(rc)
- case _ =>
- })
-
- batch_session
- }
-}
-
-class Batch_Session private(val session: Session)
-{
- val session_result = Future.promise[Int]
- @volatile var build_theories_result: Option[Promise[XML.Body]] = None
-}
-
--- a/src/Pure/PIDE/markup.ML Sat Mar 18 20:35:58 2017 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Mar 18 20:51:42 2017 +0100
@@ -194,7 +194,7 @@
val command_timing: Properties.entry
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
- val build_theories_result: string -> Properties.T
+ val build_session_finished: Properties.T
val print_operationsN: string
val print_operations: Properties.T
val debugger_state: string -> Properties.T
@@ -618,7 +618,7 @@
fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
| dest_loading_theory _ = NONE;
-fun build_theories_result id = [("function", "build_theories_result"), ("id", id)];
+val build_session_finished = [("function", "build_session_finished")];
val print_operationsN = "print_operations";
val print_operations = [(functionN, print_operationsN)];
--- a/src/Pure/PIDE/markup.scala Sat Mar 18 20:35:58 2017 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Mar 18 20:51:42 2017 +0100
@@ -541,15 +541,8 @@
}
}
- val BUILD_THEORIES_RESULT = "build_theories_result"
- object Build_Theories_Result
- {
- def unapply(props: Properties.T): Option[String] =
- props match {
- case List((FUNCTION, BUILD_THEORIES_RESULT), (ID, id)) => Some(id)
- case _ => None
- }
- }
+ val BUILD_SESSION_FINISHED = "build_session_finished"
+ val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
val PRINT_OPERATIONS = "print_operations"
--- a/src/Pure/PIDE/protocol.scala Sat Mar 18 20:35:58 2017 +0100
+++ b/src/Pure/PIDE/protocol.scala Sat Mar 18 20:51:42 2017 +0100
@@ -404,18 +404,4 @@
def dialog_result(serial: Long, result: String): Unit =
protocol_command("Document.dialog_result", Value.Long(serial), result)
-
-
- /* build_theories */
-
- def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
- {
- val symbol_codes_yxml =
- { import XML.Encode._
- YXML.string_of_body(list(pair(string, int))(Symbol.codes)) }
- val theories_yxml =
- { import XML.Encode._
- YXML.string_of_body(list(pair(Options.encode, list(Path.encode)))(theories)) }
- protocol_command("build_theories", id, master_dir.implode, theories_yxml)
- }
}
--- a/src/Pure/PIDE/session.scala Sat Mar 18 20:35:58 2017 +0100
+++ b/src/Pure/PIDE/session.scala Sat Mar 18 20:51:42 2017 +0100
@@ -514,9 +514,6 @@
prover.get.dialog_result(serial, result)
handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
- case Session.Build_Theories(id, master_dir, theories) if prover.defined =>
- prover.get.build_theories(id, master_dir, theories)
-
case Protocol_Command(name, args) if prover.defined =>
prover.get.protocol_command(name, args:_*)
@@ -600,7 +597,4 @@
def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
{ manager.send(Session.Dialog_Result(id, serial, result)) }
-
- def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
- { manager.send(Session.Build_Theories(id, master_dir, theories)) }
}
--- a/src/Pure/Tools/build.ML Sat Mar 18 20:35:58 2017 +0100
+++ b/src/Pure/Tools/build.ML Sat Mar 18 20:51:42 2017 +0100
@@ -211,36 +211,12 @@
(*PIDE version*)
val _ =
Isabelle_Process.protocol_command "build_session"
- (fn [id, yxml] =>
+ (fn [args_yxml] =>
let
- val args = decode_args yxml;
+ val args = decode_args args_yxml;
val result = (build_session args; "") handle exn =>
(Runtime.exn_message exn handle _ (*sic!*) =>
"Exception raised, but failed to print details!");
- in Output.protocol_message (Markup.build_theories_result id) [result] end | _ => raise Match);
-
-val _ =
- Isabelle_Process.protocol_command "build_theories"
- (fn [id, symbol_codes_yxml, master_dir, theories_yxml] =>
- let
- val symbols =
- YXML.parse_body symbol_codes_yxml
- |> let open XML.Decode in list (pair string int) end
- |> HTML.make_symbols;
- val theories =
- YXML.parse_body theories_yxml |>
- let open XML.Decode
- in list (pair Options.decode (list (string #> rpair Position.none))) end;
- val res1 =
- Exn.capture
- (fn () =>
- theories
- |> List.app (build_theories symbols (K Time.zeroTime) (Path.explode master_dir))) ();
- val res2 = Exn.capture Session.shutdown ();
- val result =
- (Par_Exn.release_all [res1, res2]; "") handle exn =>
- (Runtime.exn_message exn handle _ (*sic!*) =>
- "Exception raised, but failed to print details!");
- in Output.protocol_message (Markup.build_theories_result id) [result] end | _ => raise Match);
+ in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match);
end;
--- a/src/Pure/Tools/build.scala Sat Mar 18 20:35:58 2017 +0100
+++ b/src/Pure/Tools/build.scala Sat Mar 18 20:51:42 2017 +0100
@@ -130,18 +130,52 @@
}
+ /* PIDE protocol handler */
+
+ class Handler(progress: Progress, session: Session, session_name: String)
+ extends Session.Protocol_Handler
+ {
+ val result_error: Promise[String] = Future.promise
+
+ override def exit() { result_error.cancel }
+
+ private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
+ {
+ val error_message =
+ try { Pretty.string_of(YXML.parse_body(Symbol.decode(msg.text))) }
+ catch { case ERROR(msg) => msg }
+ result_error.fulfill(error_message)
+ session.send_stop()
+ true
+ }
+
+ private def loading_theory(msg: Prover.Protocol_Output): Boolean =
+ msg.properties match {
+ case Markup.Loading_Theory(name) =>
+ progress.theory(session_name, name)
+ true
+ case _ => false
+ }
+
+ val functions =
+ List(
+ Markup.BUILD_SESSION_FINISHED -> build_session_finished _,
+ Markup.LOADING_THEORY -> loading_theory _)
+ }
+
+
/* job: running prover process */
private class Job(progress: Progress,
name: String,
val info: Sessions.Info,
tree: Sessions.Tree,
+ deps: Sessions.Deps,
store: Sessions.Store,
do_output: Boolean,
verbose: Boolean,
pide: Boolean,
val numa_node: Option[Int],
- session_graph: Graph_Display.Graph,
command_timings: List[Properties.T])
{
val output = store.output_dir + Path.basic(name)
@@ -155,7 +189,7 @@
}
private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
- try { isabelle.graphview.Graph_File.write(options, graph_file, session_graph) }
+ try { isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph) }
catch { case ERROR(_) => /*error should be exposed in ML*/ }
private val future_result: Future[Process_Result] =
@@ -185,8 +219,29 @@
"ML_Heap.share_common_data (); ML_Heap.save_child " +
ML_Syntax.print_string0(File.platform_path(output))
- if (pide) {
- error("FIXME")
+ if (pide && !Sessions.pure_name(name)) {
+ val resources = new Resources(deps(parent))
+ val session = new Session(options, resources)
+ val handler = new Handler(progress, session, name)
+ session.add_protocol_handler(handler)
+
+ val session_result = Future.promise[Int]
+
+ Isabelle_Process.start(session, options, logic = parent,
+ cwd = info.dir.file, env = env, tree = Some(tree), store = store,
+ phase_changed =
+ {
+ case Session.Ready => session.protocol_command("build_session", args_yxml)
+ case Session.Terminated(rc) => session_result.fulfill(rc)
+ case _ =>
+ })
+
+ val rc = session_result.join
+
+ handler.result_error.join match {
+ case "" => Process_Result(rc)
+ case msg => Process_Result(rc max 1, out_lines = split_lines(Output.error_text(msg)))
+ }
}
else {
val args_file = Isabelle_System.tmp_file("build")
@@ -496,8 +551,8 @@
val numa_node = numa_nodes.next(used_node(_))
progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
val job =
- new Job(progress, name, info, selected_tree, store, do_output, verbose,
- pide, numa_node, deps(name).session_graph, queue.command_timings(name))
+ new Job(progress, name, info, selected_tree, deps, store, do_output, verbose,
+ pide, numa_node, queue.command_timings(name))
loop(pending, running + (name -> (ancestor_heaps, job)), results)
}
else {
@@ -679,60 +734,4 @@
sys.exit(results.rc)
})
-
-
- /* PIDE protocol */
-
- def build_theories(
- session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
- session.get_protocol_handler(classOf[Handler].getName) match {
- case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
- case _ => error("Cannot invoke build_theories: bad protocol handler")
- }
-
- class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler
- {
- private val pending = Synchronized(Map.empty[String, Promise[XML.Body]])
-
- override def exit(): Unit =
- pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
-
- def build_theories(
- session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
- {
- val promise = Future.promise[XML.Body]
- val id = Document_ID.make().toString
- pending.change(promises => promises + (id -> promise))
- session.build_theories(id, master_dir, theories)
- promise
- }
-
- private def loading_theory(msg: Prover.Protocol_Output): Boolean =
- msg.properties match {
- case Markup.Loading_Theory(name) => progress.theory(session_name, name); true
- case _ => false
- }
-
- private def build_theories_result(msg: Prover.Protocol_Output): Boolean =
- msg.properties match {
- case Markup.Build_Theories_Result(id) =>
- pending.change_result(promises =>
- promises.get(id) match {
- case Some(promise) =>
- val error_message =
- try { YXML.parse_body(Symbol.decode(msg.text)) }
- catch { case exn: Throwable => List(XML.Text(Exn.message(exn))) }
- promise.fulfill(error_message)
- (true, promises - id)
- case None =>
- (false, promises)
- })
- case _ => false
- }
-
- val functions =
- List(
- Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
- Markup.LOADING_THEORY -> loading_theory _)
- }
}
--- a/src/Pure/build-jars Sat Mar 18 20:35:58 2017 +0100
+++ b/src/Pure/build-jars Sat Mar 18 20:51:42 2017 +0100
@@ -84,7 +84,6 @@
Isar/token.scala
ML/ml_lex.scala
ML/ml_syntax.scala
- PIDE/batch_session.scala
PIDE/command.scala
PIDE/command_span.scala
PIDE/document.scala