# HG changeset patch # User wenzelm # Date 1421249239 -3600 # Node ID e94df7f6b608b0648ccc0a25d394a4c35fcbfb11 # Parent b5d43b01a6b365149a2ed5a59d4b48c2b252c44b clarified build_theories: proper protocol handler; diff -r b5d43b01a6b3 -r e94df7f6b608 src/Pure/PIDE/batch_session.scala --- a/src/Pure/PIDE/batch_session.scala Wed Jan 14 16:23:33 2015 +0100 +++ b/src/Pure/PIDE/batch_session.scala Wed Jan 14 16:27:19 2015 +0100 @@ -16,7 +16,7 @@ options: Options, verbose: Boolean = false, dirs: List[Path] = Nil, - session: String) + session: String): Boolean = { val (_, session_tree) = Build.find_sessions(options, dirs).selection(false, false, Nil, List(session)) @@ -37,22 +37,24 @@ } val progress = new Build.Console_Progress(verbose) - val result = Future.promise[Unit] + + val session_result = Future.promise[Unit] + @volatile var build_theories_result: Option[Promise[Boolean]] = None val prover_session = new Session(resources) prover_session.phase_changed += Session.Consumer[Session.Phase](getClass.getName) { case Session.Ready => - val id = Document_ID.make().toString + prover_session.add_protocol_handler(Build.handler_name) val master_dir = session_info.dir val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) }) - prover_session.build_theories(id, master_dir, theories) - // FIXME proper check of result!? + build_theories_result = + Some(Build.build_theories(prover_session, master_dir, theories)) case Session.Inactive | Session.Failed => - result.fulfill_result(Exn.Exn(ERROR("Prover process terminated"))) + session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated"))) case Session.Shutdown => - result.fulfill(()) + session_result.fulfill(()) case _ => } @@ -68,7 +70,11 @@ prover_session.start("Isabelle", List("-r", "-q", parent_session)) - result.join + session_result.join + build_theories_result match { + case None => false + case Some(promise) => promise.join + } } } diff -r b5d43b01a6b3 -r e94df7f6b608 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Jan 14 16:23:33 2015 +0100 +++ b/src/Pure/PIDE/markup.scala Wed Jan 14 16:27:19 2015 +0100 @@ -467,11 +467,12 @@ } } + val BUILD_THEORIES_RESULT = "build_theories_result" object Build_Theories_Result { def unapply(props: Properties.T): Option[(String, Boolean)] = props match { - case List((FUNCTION, "build_theories_result"), + case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok)) case _ => None } diff -r b5d43b01a6b3 -r e94df7f6b608 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Wed Jan 14 16:23:33 2015 +0100 +++ b/src/Pure/PIDE/protocol.ML Wed Jan 14 16:27:19 2015 +0100 @@ -111,23 +111,6 @@ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn); val _ = - Isabelle_Process.protocol_command "build_theories" - (fn [id, master_dir, theories_yxml] => - let - val theories = - YXML.parse_body theories_yxml |> - let open XML.Decode - in list (pair Options.decode (list (string #> rpair Position.none))) end; - val result = - Exn.capture (fn () => - theories |> List.app (Thy_Info.build_theories (K NONE) (Path.explode master_dir))) (); - val ok = - (case result of - Exn.Res _ => true - | Exn.Exn exn => (Runtime.exn_error_message exn; false)); - in Output.protocol_message (Markup.build_theories_result id ok) [] end); - -val _ = Isabelle_Process.protocol_command "ML_System.share_common_data" (fn [] => ML_System.share_common_data ()); diff -r b5d43b01a6b3 -r e94df7f6b608 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Wed Jan 14 16:23:33 2015 +0100 +++ b/src/Pure/PIDE/session.scala Wed Jan 14 16:27:19 2015 +0100 @@ -105,7 +105,7 @@ val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean] } - class Protocol_Handlers( + private class Protocol_Handlers( handlers: Map[String, Session.Protocol_Handler] = Map.empty, functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty) { @@ -237,14 +237,6 @@ resources.base_syntax - /* protocol handlers */ - - @volatile private var _protocol_handlers = new Session.Protocol_Handlers() - - def protocol_handler(name: String): Option[Session.Protocol_Handler] = - _protocol_handlers.get(name) - - /* theory files */ def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text = @@ -343,6 +335,17 @@ } + /* protocol handlers */ + + private val _protocol_handlers = Synchronized(new Session.Protocol_Handlers) + + def get_protocol_handler(name: String): Option[Session.Protocol_Handler] = + _protocol_handlers.value.get(name) + + def add_protocol_handler(name: String): Unit = + _protocol_handlers.change(_.add(prover.get, name)) + + /* manager thread */ private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) } @@ -432,11 +435,11 @@ output match { case msg: Prover.Protocol_Output => - val handled = _protocol_handlers.invoke(msg) + val handled = _protocol_handlers.value.invoke(msg) if (!handled) { msg.properties match { case Markup.Protocol_Handler(name) if prover.defined => - _protocol_handlers = _protocol_handlers.add(prover.get, name) + add_protocol_handler(name) case Protocol.Command_Timing(state_id, timing) if prover.defined => val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) @@ -525,7 +528,7 @@ case Stop => if (prover.defined && is_ready) { - _protocol_handlers = _protocol_handlers.stop(prover.get) + _protocol_handlers.change(_.stop(prover.get)) global_state.change(_ => Document.State.init) phase = Session.Shutdown prover.get.terminate diff -r b5d43b01a6b3 -r e94df7f6b608 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Jan 14 16:23:33 2015 +0100 +++ b/src/Pure/Thy/thy_info.ML Wed Jan 14 16:27:19 2015 +0100 @@ -12,10 +12,11 @@ val get_theory: string -> theory val master_directory: string -> Path.T val remove_thy: string -> unit + val use_theories: + {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} -> + (string * Position.T) list -> unit val use_thys: (string * Position.T) list -> unit val use_thy: string * Position.T -> unit - val build_theories: (Toplevel.transition -> Time.time option) -> Path.T -> - Options.T * (string * Position.T) list -> unit val script_thy: Position.T -> string -> theory -> theory val register_thy: theory -> unit val finish: unit -> unit @@ -343,31 +344,6 @@ val use_thy = use_thys o single; -(* theories in batch build *) - -fun build_theories last_timing master_dir (options, thys) = - let - val condition = space_explode "," (Options.string options "condition"); - val conds = filter_out (can getenv_strict) condition; - in - if null conds then - (Options.set_default options; - (use_theories { - document = Present.document_enabled (Options.string options "document"), - last_timing = last_timing, - master_dir = master_dir} - |> Unsynchronized.setmp print_mode - (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) - |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs") - |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") - |> Multithreading.max_threads_setmp (Options.int options "threads") - |> Unsynchronized.setmp Future.ML_statistics true) thys) - else - Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ - " (undefined " ^ commas conds ^ ")\n") - end; - - (* toplevel scripting -- without maintaining database *) fun script_thy pos txt thy = diff -r b5d43b01a6b3 -r e94df7f6b608 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Wed Jan 14 16:23:33 2015 +0100 +++ b/src/Pure/Tools/build.ML Wed Jan 14 16:27:19 2015 +0100 @@ -97,6 +97,28 @@ (* build *) +fun build_theories last_timing master_dir (options, thys) = + let + val condition = space_explode "," (Options.string options "condition"); + val conds = filter_out (can getenv_strict) condition; + in + if null conds then + (Options.set_default options; + (Thy_Info.use_theories { + document = Present.document_enabled (Options.string options "document"), + last_timing = last_timing, + master_dir = master_dir} + |> Unsynchronized.setmp print_mode + (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) + |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs") + |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") + |> Multithreading.max_threads_setmp (Options.int options "threads") + |> Unsynchronized.setmp Future.ML_statistics true) thys) + else + Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ + " (undefined " ^ commas conds ^ ")\n") + end; + fun build args_file = Command_Line.tool0 (fn () => let val _ = SHA1_Samples.test (); @@ -129,7 +151,7 @@ val res1 = theories |> - (List.app (Thy_Info.build_theories last_timing Path.current) + (List.app (build_theories last_timing Path.current) |> session_timing name verbose |> Unsynchronized.setmp Output.protocol_message_fn protocol_message |> Multithreading.max_threads_setmp (Options.int options "threads") @@ -141,4 +163,24 @@ val _ = if do_output then () else exit 0; in () end); + +(* PIDE protocol *) + +val _ = + Isabelle_Process.protocol_command "build_theories" + (fn [id, master_dir, theories_yxml] => + let + val theories = + YXML.parse_body theories_yxml |> + let open XML.Decode + in list (pair Options.decode (list (string #> rpair Position.none))) end; + val result = + Exn.capture (fn () => + theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) (); + val ok = + (case result of + Exn.Res _ => true + | Exn.Exn exn => (Runtime.exn_error_message exn; false)); + in Output.protocol_message (Markup.build_theories_result id ok) [] end); + end; diff -r b5d43b01a6b3 -r e94df7f6b608 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Jan 14 16:23:33 2015 +0100 +++ b/src/Pure/Tools/build.scala Wed Jan 14 16:27:19 2015 +0100 @@ -1025,5 +1025,48 @@ } } } + + + /* PIDE protocol */ + + val handler_name = "isabelle.Build$Handler" + + def build_theories( + session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] = + session.get_protocol_handler(handler_name) match { + case Some(handler: Handler) => handler.build_theories(session, master_dir, theories) + case _ => error("Cannot invoke build_theories: bad protocol handler") + } + + class Handler extends Session.Protocol_Handler + { + private val pending = Synchronized(Map.empty[String, Promise[Boolean]]) + + def build_theories( + session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] = + { + val promise = Future.promise[Boolean] + val id = Document_ID.make().toString + pending.change(promises => promises + (id -> promise)) + session.build_theories(id, master_dir, theories) + promise + } + + private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean = + msg.properties match { + case Markup.Build_Theories_Result(id, ok) => + pending.change_result(promises => + promises.get(id) match { + case Some(promise) => promise.fulfill(ok); (true, promises - id) + case None => (false, promises) + }) + case _ => false + } + + override def stop(prover: Prover): Unit = + pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty }) + + val functions = Map(Markup.BUILD_THEORIES_RESULT -> build_theories_result _) + } } diff -r b5d43b01a6b3 -r e94df7f6b608 src/Pure/Tools/print_operation.scala --- a/src/Pure/Tools/print_operation.scala Wed Jan 14 16:23:33 2015 +0100 +++ b/src/Pure/Tools/print_operation.scala Wed Jan 14 16:27:19 2015 +0100 @@ -10,7 +10,7 @@ object Print_Operation { def print_operations(session: Session): List[(String, String)] = - session.protocol_handler("isabelle.Print_Operation$Handler") match { + session.get_protocol_handler("isabelle.Print_Operation$Handler") match { case Some(handler: Handler) => handler.get case _ => Nil }