clarified build_theories: proper protocol handler;

--- 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
+    }
   }
 }
 

--- 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
       }

--- 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 ());
 

--- 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

--- 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 =

--- 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;

--- 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 _)
+  }
 }
 

--- 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
     }