more informative build_theories_result: cumulative Runtime.exn_message;
authorwenzelm
Thu Jan 15 12:54:08 2015 +0100 (2015-01-15)
changeset 593697090199d3f78
parent 59368 100db5cf5be5
child 59370 b13ff987c559
more informative build_theories_result: cumulative Runtime.exn_message;
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/session.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Thu Jan 15 11:39:58 2015 +0100
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Thu Jan 15 12:54:08 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): Boolean =
     1.8 +    session: String): Batch_Session =
     1.9    {
    1.10      val (_, session_tree) =
    1.11        Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
    1.12 @@ -38,10 +38,8 @@
    1.13  
    1.14      val progress = new Build.Console_Progress(verbose)
    1.15  
    1.16 -    val session_result = Future.promise[Unit]
    1.17 -    @volatile var build_theories_result: Option[Promise[Boolean]] = None
    1.18 -
    1.19      val prover_session = new Session(resources)
    1.20 +    val batch_session = new Batch_Session(prover_session)
    1.21  
    1.22      val handler = new Build.Handler(progress, session)
    1.23  
    1.24 @@ -51,22 +49,24 @@
    1.25            prover_session.add_protocol_handler(handler)
    1.26            val master_dir = session_info.dir
    1.27            val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
    1.28 -          build_theories_result =
    1.29 +          batch_session.build_theories_result =
    1.30              Some(Build.build_theories(prover_session, master_dir, theories))
    1.31          case Session.Inactive | Session.Failed =>
    1.32 -          session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
    1.33 +          batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
    1.34          case Session.Shutdown =>
    1.35 -          session_result.fulfill(())
    1.36 +          batch_session.session_result.fulfill(())
    1.37          case _ =>
    1.38        }
    1.39  
    1.40      prover_session.start("Isabelle", List("-r", "-q", parent_session))
    1.41  
    1.42 -    session_result.join
    1.43 -    build_theories_result match {
    1.44 -      case None => false
    1.45 -      case Some(promise) => promise.join
    1.46 -    }
    1.47 +    batch_session
    1.48    }
    1.49  }
    1.50  
    1.51 +class Batch_Session private(val session: Session)
    1.52 +{
    1.53 +  val session_result = Future.promise[Unit]
    1.54 +  @volatile var build_theories_result: Option[Promise[XML.Body]] = None
    1.55 +}
    1.56 +
     2.1 --- a/src/Pure/PIDE/markup.ML	Thu Jan 15 11:39:58 2015 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Thu Jan 15 12:54:08 2015 +0100
     2.3 @@ -186,7 +186,7 @@
     2.4    val command_timing: Properties.entry
     2.5    val loading_theory: string -> Properties.T
     2.6    val dest_loading_theory: Properties.T -> string option
     2.7 -  val build_theories_result: string -> bool -> Properties.T
     2.8 +  val build_theories_result: string -> Properties.T
     2.9    val print_operationsN: string
    2.10    val print_operations: Properties.T
    2.11    val simp_trace_panelN: string
    2.12 @@ -597,8 +597,7 @@
    2.13  fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
    2.14    | dest_loading_theory _ = NONE;
    2.15  
    2.16 -fun build_theories_result id ok =
    2.17 -  [("function", "build_theories_result"), ("id", id), ("ok", print_bool ok)];
    2.18 +fun build_theories_result id = [("function", "build_theories_result"), ("id", id)];
    2.19  
    2.20  val print_operationsN = "print_operations";
    2.21  val print_operations = [(functionN, print_operationsN)];
     3.1 --- a/src/Pure/PIDE/markup.scala	Thu Jan 15 11:39:58 2015 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Thu Jan 15 12:54:08 2015 +0100
     3.3 @@ -471,10 +471,9 @@
     3.4    val BUILD_THEORIES_RESULT = "build_theories_result"
     3.5    object Build_Theories_Result
     3.6    {
     3.7 -    def unapply(props: Properties.T): Option[(String, Boolean)] =
     3.8 +    def unapply(props: Properties.T): Option[String] =
     3.9        props match {
    3.10 -        case List((FUNCTION, BUILD_THEORIES_RESULT),
    3.11 -          ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
    3.12 +        case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id)) => Some(id)
    3.13          case _ => None
    3.14        }
    3.15    }
     4.1 --- a/src/Pure/PIDE/session.ML	Thu Jan 15 11:39:58 2015 +0100
     4.2 +++ b/src/Pure/PIDE/session.ML	Thu Jan 15 12:54:08 2015 +0100
     4.3 @@ -11,6 +11,7 @@
     4.4    val get_keywords: unit -> Keyword.keywords
     4.5    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     4.6      (Path.T * Path.T) list -> string -> string * string -> bool -> unit
     4.7 +  val shutdown: unit -> unit
     4.8    val finish: unit -> unit
     4.9    val save: string -> unit
    4.10    val protocol_handler: string -> unit
    4.11 @@ -58,22 +59,23 @@
    4.12  
    4.13  (* finish *)
    4.14  
    4.15 +fun shutdown () =
    4.16 + (Execution.shutdown ();
    4.17 +  Event_Timer.shutdown ();
    4.18 +  Future.shutdown ());
    4.19 +
    4.20  fun finish () =
    4.21 - (Execution.shutdown ();
    4.22 + (shutdown ();
    4.23    Thy_Info.finish ();
    4.24    Present.finish ();
    4.25 -  Future.shutdown ();
    4.26 -  Event_Timer.shutdown ();
    4.27 -  Future.shutdown ();
    4.28 +  shutdown ();
    4.29    keywords :=
    4.30      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
    4.31        (Thy_Info.get_names ()) Keyword.empty_keywords;
    4.32    session_finished := true);
    4.33  
    4.34  fun save heap =
    4.35 - (Execution.shutdown ();
    4.36 -  Event_Timer.shutdown ();
    4.37 -  Future.shutdown ();
    4.38 + (shutdown ();
    4.39    ML_System.share_common_data ();
    4.40    ML_System.save_state heap);
    4.41  
     5.1 --- a/src/Pure/Tools/build.ML	Thu Jan 15 11:39:58 2015 +0100
     5.2 +++ b/src/Pure/Tools/build.ML	Thu Jan 15 12:54:08 2015 +0100
     5.3 @@ -174,13 +174,14 @@
     5.4            YXML.parse_body theories_yxml |>
     5.5              let open XML.Decode
     5.6              in list (pair Options.decode (list (string #> rpair Position.none))) end;
     5.7 -        val result =
     5.8 +        val res1 =
     5.9            Exn.capture (fn () =>
    5.10              theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) ();
    5.11 -        val ok =
    5.12 -          (case result of
    5.13 -            Exn.Res _ => true
    5.14 -          | Exn.Exn exn => (Runtime.exn_error_message exn; false));
    5.15 -    in Output.protocol_message (Markup.build_theories_result id ok) [] end);
    5.16 +        val res2 = Exn.capture Session.shutdown ();
    5.17 +        val result =
    5.18 +          (Par_Exn.release_all [res1, res2]; "") handle exn =>
    5.19 +            (Runtime.exn_message exn handle _ (*sic!*) =>
    5.20 +              "Exception raised, but failed to print details!");
    5.21 +    in Output.protocol_message (Markup.build_theories_result id) [result] end);
    5.22  
    5.23  end;
     6.1 --- a/src/Pure/Tools/build.scala	Thu Jan 15 11:39:58 2015 +0100
     6.2 +++ b/src/Pure/Tools/build.scala	Thu Jan 15 12:54:08 2015 +0100
     6.3 @@ -1030,7 +1030,7 @@
     6.4    /* PIDE protocol */
     6.5  
     6.6    def build_theories(
     6.7 -    session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
     6.8 +    session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
     6.9        session.get_protocol_handler(classOf[Handler].getName) match {
    6.10          case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
    6.11          case _ => error("Cannot invoke build_theories: bad protocol handler")
    6.12 @@ -1038,12 +1038,12 @@
    6.13  
    6.14    class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler
    6.15    {
    6.16 -    private val pending = Synchronized(Map.empty[String, Promise[Boolean]])
    6.17 +    private val pending = Synchronized(Map.empty[String, Promise[XML.Body]])
    6.18  
    6.19      def build_theories(
    6.20 -      session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
    6.21 +      session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
    6.22      {
    6.23 -      val promise = Future.promise[Boolean]
    6.24 +      val promise = Future.promise[XML.Body]
    6.25        val id = Document_ID.make().toString
    6.26        pending.change(promises => promises + (id -> promise))
    6.27        session.build_theories(id, master_dir, theories)
    6.28 @@ -1058,11 +1058,17 @@
    6.29  
    6.30      private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    6.31        msg.properties match {
    6.32 -        case Markup.Build_Theories_Result(id, ok) =>
    6.33 +        case Markup.Build_Theories_Result(id) =>
    6.34            pending.change_result(promises =>
    6.35              promises.get(id) match {
    6.36 -              case Some(promise) => promise.fulfill(ok); (true, promises - id)
    6.37 -              case None => (false, promises)
    6.38 +              case Some(promise) =>
    6.39 +                val error_message =
    6.40 +                  try { YXML.parse_body(Symbol.decode(msg.text)) }
    6.41 +                  catch { case exn: Throwable => List(XML.Text(Exn.message(exn))) }
    6.42 +                promise.fulfill(error_message)
    6.43 +                (true, promises - id)
    6.44 +              case None =>
    6.45 +                (false, promises)
    6.46              })
    6.47          case _ => false
    6.48        }