# HG changeset patch # User wenzelm # Date 1489866702 -3600 # Node ID 347ed6219dabaa0661ad60d862f4dd814a9341ac # Parent 34d56ca5b548e9b9720ac67d02c3d60799d84254 more realistic PIDE build session; diff -r 34d56ca5b548 -r 347ed6219dab src/Pure/PIDE/batch_session.scala --- 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 -} - diff -r 34d56ca5b548 -r 347ed6219dab src/Pure/PIDE/markup.ML --- 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)]; diff -r 34d56ca5b548 -r 347ed6219dab src/Pure/PIDE/markup.scala --- 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" diff -r 34d56ca5b548 -r 347ed6219dab src/Pure/PIDE/protocol.scala --- 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) - } } diff -r 34d56ca5b548 -r 347ed6219dab src/Pure/PIDE/session.scala --- 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)) } } diff -r 34d56ca5b548 -r 347ed6219dab src/Pure/Tools/build.ML --- 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; diff -r 34d56ca5b548 -r 347ed6219dab src/Pure/Tools/build.scala --- 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 _) - } } diff -r 34d56ca5b548 -r 347ed6219dab src/Pure/build-jars --- 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