clarified build_theories: proper protocol handler;
authorwenzelm
Wed Jan 14 16:27:19 2015 +0100 (2015-01-14)
changeset 59366e94df7f6b608
parent 59365 b5d43b01a6b3
child 59367 6193bbbbe564
clarified build_theories: proper protocol handler;
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/print_operation.scala
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Wed Jan 14 16:23:33 2015 +0100
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Wed Jan 14 16:27:19 2015 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4      options: Options,
     1.5      verbose: Boolean = false,
     1.6      dirs: List[Path] = Nil,
     1.7 -    session: String)
     1.8 +    session: String): Boolean =
     1.9    {
    1.10      val (_, session_tree) =
    1.11        Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
    1.12 @@ -37,22 +37,24 @@
    1.13      }
    1.14  
    1.15      val progress = new Build.Console_Progress(verbose)
    1.16 -    val result = Future.promise[Unit]
    1.17 +
    1.18 +    val session_result = Future.promise[Unit]
    1.19 +    @volatile var build_theories_result: Option[Promise[Boolean]] = None
    1.20  
    1.21      val prover_session = new Session(resources)
    1.22  
    1.23      prover_session.phase_changed +=
    1.24        Session.Consumer[Session.Phase](getClass.getName) {
    1.25          case Session.Ready =>
    1.26 -          val id = Document_ID.make().toString
    1.27 +          prover_session.add_protocol_handler(Build.handler_name)
    1.28            val master_dir = session_info.dir
    1.29            val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
    1.30 -          prover_session.build_theories(id, master_dir, theories)
    1.31 -          // FIXME proper check of result!?
    1.32 +          build_theories_result =
    1.33 +            Some(Build.build_theories(prover_session, master_dir, theories))
    1.34          case Session.Inactive | Session.Failed =>
    1.35 -          result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
    1.36 +          session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
    1.37          case Session.Shutdown =>
    1.38 -          result.fulfill(())
    1.39 +          session_result.fulfill(())
    1.40          case _ =>
    1.41        }
    1.42  
    1.43 @@ -68,7 +70,11 @@
    1.44  
    1.45      prover_session.start("Isabelle", List("-r", "-q", parent_session))
    1.46  
    1.47 -    result.join
    1.48 +    session_result.join
    1.49 +    build_theories_result match {
    1.50 +      case None => false
    1.51 +      case Some(promise) => promise.join
    1.52 +    }
    1.53    }
    1.54  }
    1.55  
     2.1 --- a/src/Pure/PIDE/markup.scala	Wed Jan 14 16:23:33 2015 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jan 14 16:27:19 2015 +0100
     2.3 @@ -467,11 +467,12 @@
     2.4        }
     2.5    }
     2.6  
     2.7 +  val BUILD_THEORIES_RESULT = "build_theories_result"
     2.8    object Build_Theories_Result
     2.9    {
    2.10      def unapply(props: Properties.T): Option[(String, Boolean)] =
    2.11        props match {
    2.12 -        case List((FUNCTION, "build_theories_result"),
    2.13 +        case List((FUNCTION, BUILD_THEORIES_RESULT),
    2.14            ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
    2.15          case _ => None
    2.16        }
     3.1 --- a/src/Pure/PIDE/protocol.ML	Wed Jan 14 16:23:33 2015 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Jan 14 16:27:19 2015 +0100
     3.3 @@ -111,23 +111,6 @@
     3.4          handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
     3.5  
     3.6  val _ =
     3.7 -  Isabelle_Process.protocol_command "build_theories"
     3.8 -    (fn [id, master_dir, theories_yxml] =>
     3.9 -      let
    3.10 -        val theories =
    3.11 -          YXML.parse_body theories_yxml |>
    3.12 -            let open XML.Decode
    3.13 -            in list (pair Options.decode (list (string #> rpair Position.none))) end;
    3.14 -        val result =
    3.15 -          Exn.capture (fn () =>
    3.16 -            theories |> List.app (Thy_Info.build_theories (K NONE) (Path.explode master_dir))) ();
    3.17 -        val ok =
    3.18 -          (case result of
    3.19 -            Exn.Res _ => true
    3.20 -          | Exn.Exn exn => (Runtime.exn_error_message exn; false));
    3.21 -    in Output.protocol_message (Markup.build_theories_result id ok) [] end);
    3.22 -
    3.23 -val _ =
    3.24    Isabelle_Process.protocol_command "ML_System.share_common_data"
    3.25      (fn [] => ML_System.share_common_data ());
    3.26  
     4.1 --- a/src/Pure/PIDE/session.scala	Wed Jan 14 16:23:33 2015 +0100
     4.2 +++ b/src/Pure/PIDE/session.scala	Wed Jan 14 16:27:19 2015 +0100
     4.3 @@ -105,7 +105,7 @@
     4.4      val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
     4.5    }
     4.6  
     4.7 -  class Protocol_Handlers(
     4.8 +  private class Protocol_Handlers(
     4.9      handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    4.10      functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
    4.11    {
    4.12 @@ -237,14 +237,6 @@
    4.13      resources.base_syntax
    4.14  
    4.15  
    4.16 -  /* protocol handlers */
    4.17 -
    4.18 -  @volatile private var _protocol_handlers = new Session.Protocol_Handlers()
    4.19 -
    4.20 -  def protocol_handler(name: String): Option[Session.Protocol_Handler] =
    4.21 -    _protocol_handlers.get(name)
    4.22 -
    4.23 -
    4.24    /* theory files */
    4.25  
    4.26    def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
    4.27 @@ -343,6 +335,17 @@
    4.28    }
    4.29  
    4.30  
    4.31 +  /* protocol handlers */
    4.32 +
    4.33 +  private val _protocol_handlers = Synchronized(new Session.Protocol_Handlers)
    4.34 +
    4.35 +  def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
    4.36 +    _protocol_handlers.value.get(name)
    4.37 +
    4.38 +  def add_protocol_handler(name: String): Unit =
    4.39 +    _protocol_handlers.change(_.add(prover.get, name))
    4.40 +
    4.41 +
    4.42    /* manager thread */
    4.43  
    4.44    private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
    4.45 @@ -432,11 +435,11 @@
    4.46  
    4.47        output match {
    4.48          case msg: Prover.Protocol_Output =>
    4.49 -          val handled = _protocol_handlers.invoke(msg)
    4.50 +          val handled = _protocol_handlers.value.invoke(msg)
    4.51            if (!handled) {
    4.52              msg.properties match {
    4.53                case Markup.Protocol_Handler(name) if prover.defined =>
    4.54 -                _protocol_handlers = _protocol_handlers.add(prover.get, name)
    4.55 +                add_protocol_handler(name)
    4.56  
    4.57                case Protocol.Command_Timing(state_id, timing) if prover.defined =>
    4.58                  val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
    4.59 @@ -525,7 +528,7 @@
    4.60  
    4.61            case Stop =>
    4.62              if (prover.defined && is_ready) {
    4.63 -              _protocol_handlers = _protocol_handlers.stop(prover.get)
    4.64 +              _protocol_handlers.change(_.stop(prover.get))
    4.65                global_state.change(_ => Document.State.init)
    4.66                phase = Session.Shutdown
    4.67                prover.get.terminate
     5.1 --- a/src/Pure/Thy/thy_info.ML	Wed Jan 14 16:23:33 2015 +0100
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jan 14 16:27:19 2015 +0100
     5.3 @@ -12,10 +12,11 @@
     5.4    val get_theory: string -> theory
     5.5    val master_directory: string -> Path.T
     5.6    val remove_thy: string -> unit
     5.7 +  val use_theories:
     5.8 +    {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
     5.9 +    (string * Position.T) list -> unit
    5.10    val use_thys: (string * Position.T) list -> unit
    5.11    val use_thy: string * Position.T -> unit
    5.12 -  val build_theories: (Toplevel.transition -> Time.time option) -> Path.T ->
    5.13 -    Options.T * (string * Position.T) list -> unit
    5.14    val script_thy: Position.T -> string -> theory -> theory
    5.15    val register_thy: theory -> unit
    5.16    val finish: unit -> unit
    5.17 @@ -343,31 +344,6 @@
    5.18  val use_thy = use_thys o single;
    5.19  
    5.20  
    5.21 -(* theories in batch build *)
    5.22 -
    5.23 -fun build_theories last_timing master_dir (options, thys) =
    5.24 -  let
    5.25 -    val condition = space_explode "," (Options.string options "condition");
    5.26 -    val conds = filter_out (can getenv_strict) condition;
    5.27 -  in
    5.28 -    if null conds then
    5.29 -      (Options.set_default options;
    5.30 -        (use_theories {
    5.31 -          document = Present.document_enabled (Options.string options "document"),
    5.32 -          last_timing = last_timing,
    5.33 -          master_dir = master_dir}
    5.34 -        |> Unsynchronized.setmp print_mode
    5.35 -            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    5.36 -        |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    5.37 -        |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    5.38 -        |> Multithreading.max_threads_setmp (Options.int options "threads")
    5.39 -        |> Unsynchronized.setmp Future.ML_statistics true) thys)
    5.40 -    else
    5.41 -      Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
    5.42 -        " (undefined " ^ commas conds ^ ")\n")
    5.43 -  end;
    5.44 -
    5.45 -
    5.46  (* toplevel scripting -- without maintaining database *)
    5.47  
    5.48  fun script_thy pos txt thy =
     6.1 --- a/src/Pure/Tools/build.ML	Wed Jan 14 16:23:33 2015 +0100
     6.2 +++ b/src/Pure/Tools/build.ML	Wed Jan 14 16:27:19 2015 +0100
     6.3 @@ -97,6 +97,28 @@
     6.4  
     6.5  (* build *)
     6.6  
     6.7 +fun build_theories last_timing master_dir (options, thys) =
     6.8 +  let
     6.9 +    val condition = space_explode "," (Options.string options "condition");
    6.10 +    val conds = filter_out (can getenv_strict) condition;
    6.11 +  in
    6.12 +    if null conds then
    6.13 +      (Options.set_default options;
    6.14 +        (Thy_Info.use_theories {
    6.15 +          document = Present.document_enabled (Options.string options "document"),
    6.16 +          last_timing = last_timing,
    6.17 +          master_dir = master_dir}
    6.18 +        |> Unsynchronized.setmp print_mode
    6.19 +            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    6.20 +        |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    6.21 +        |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    6.22 +        |> Multithreading.max_threads_setmp (Options.int options "threads")
    6.23 +        |> Unsynchronized.setmp Future.ML_statistics true) thys)
    6.24 +    else
    6.25 +      Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
    6.26 +        " (undefined " ^ commas conds ^ ")\n")
    6.27 +  end;
    6.28 +
    6.29  fun build args_file = Command_Line.tool0 (fn () =>
    6.30      let
    6.31        val _ = SHA1_Samples.test ();
    6.32 @@ -129,7 +151,7 @@
    6.33  
    6.34        val res1 =
    6.35          theories |>
    6.36 -          (List.app (Thy_Info.build_theories last_timing Path.current)
    6.37 +          (List.app (build_theories last_timing Path.current)
    6.38              |> session_timing name verbose
    6.39              |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
    6.40              |> Multithreading.max_threads_setmp (Options.int options "threads")
    6.41 @@ -141,4 +163,24 @@
    6.42        val _ = if do_output then () else exit 0;
    6.43      in () end);
    6.44  
    6.45 +
    6.46 +(* PIDE protocol *)
    6.47 +
    6.48 +val _ =
    6.49 +  Isabelle_Process.protocol_command "build_theories"
    6.50 +    (fn [id, master_dir, theories_yxml] =>
    6.51 +      let
    6.52 +        val theories =
    6.53 +          YXML.parse_body theories_yxml |>
    6.54 +            let open XML.Decode
    6.55 +            in list (pair Options.decode (list (string #> rpair Position.none))) end;
    6.56 +        val result =
    6.57 +          Exn.capture (fn () =>
    6.58 +            theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) ();
    6.59 +        val ok =
    6.60 +          (case result of
    6.61 +            Exn.Res _ => true
    6.62 +          | Exn.Exn exn => (Runtime.exn_error_message exn; false));
    6.63 +    in Output.protocol_message (Markup.build_theories_result id ok) [] end);
    6.64 +
    6.65  end;
     7.1 --- a/src/Pure/Tools/build.scala	Wed Jan 14 16:23:33 2015 +0100
     7.2 +++ b/src/Pure/Tools/build.scala	Wed Jan 14 16:27:19 2015 +0100
     7.3 @@ -1025,5 +1025,48 @@
     7.4        }
     7.5      }
     7.6    }
     7.7 +
     7.8 +
     7.9 +  /* PIDE protocol */
    7.10 +
    7.11 +  val handler_name = "isabelle.Build$Handler"
    7.12 +
    7.13 +  def build_theories(
    7.14 +    session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
    7.15 +      session.get_protocol_handler(handler_name) match {
    7.16 +        case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
    7.17 +        case _ => error("Cannot invoke build_theories: bad protocol handler")
    7.18 +      }
    7.19 +
    7.20 +  class Handler extends Session.Protocol_Handler
    7.21 +  {
    7.22 +    private val pending = Synchronized(Map.empty[String, Promise[Boolean]])
    7.23 +
    7.24 +    def build_theories(
    7.25 +      session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
    7.26 +    {
    7.27 +      val promise = Future.promise[Boolean]
    7.28 +      val id = Document_ID.make().toString
    7.29 +      pending.change(promises => promises + (id -> promise))
    7.30 +      session.build_theories(id, master_dir, theories)
    7.31 +      promise
    7.32 +    }
    7.33 +
    7.34 +    private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    7.35 +      msg.properties match {
    7.36 +        case Markup.Build_Theories_Result(id, ok) =>
    7.37 +          pending.change_result(promises =>
    7.38 +            promises.get(id) match {
    7.39 +              case Some(promise) => promise.fulfill(ok); (true, promises - id)
    7.40 +              case None => (false, promises)
    7.41 +            })
    7.42 +        case _ => false
    7.43 +      }
    7.44 +
    7.45 +    override def stop(prover: Prover): Unit =
    7.46 +      pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
    7.47 +
    7.48 +    val functions = Map(Markup.BUILD_THEORIES_RESULT -> build_theories_result _)
    7.49 +  }
    7.50  }
    7.51  
     8.1 --- a/src/Pure/Tools/print_operation.scala	Wed Jan 14 16:23:33 2015 +0100
     8.2 +++ b/src/Pure/Tools/print_operation.scala	Wed Jan 14 16:27:19 2015 +0100
     8.3 @@ -10,7 +10,7 @@
     8.4  object Print_Operation
     8.5  {
     8.6    def print_operations(session: Session): List[(String, String)] =
     8.7 -    session.protocol_handler("isabelle.Print_Operation$Handler") match {
     8.8 +    session.get_protocol_handler("isabelle.Print_Operation$Handler") match {
     8.9        case Some(handler: Handler) => handler.get
    8.10        case _ => Nil
    8.11      }