more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
authorwenzelm
Thu Dec 05 20:22:53 2013 +0100 (2013-12-05 ago)
changeset 5467887910da843d5
parent 54677 ae5426994961
child 54679 88adcd3b34e8
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
tuned signature;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Dec 05 20:06:28 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Dec 05 20:22:53 2013 +0100
     1.3 @@ -88,7 +88,6 @@
     1.4    val unknown_proof: transition -> transition
     1.5    val unknown_context: transition -> transition
     1.6    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
     1.7 -  val status: transition -> Markup.T -> unit
     1.8    val add_hook: (transition -> state -> state -> unit) -> unit
     1.9    val get_timing: transition -> Time.time option
    1.10    val put_timing: Time.time option -> transition -> transition
    1.11 @@ -586,9 +585,6 @@
    1.12  fun setmp_thread_position (Transition {pos, ...}) f x =
    1.13    Position.setmp_thread_data pos f x;
    1.14  
    1.15 -fun status tr m =
    1.16 -  setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
    1.17 -
    1.18  
    1.19  (* post-transition hooks *)
    1.20  
     2.1 --- a/src/Pure/PIDE/command.ML	Thu Dec 05 20:06:28 2013 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Thu Dec 05 20:22:53 2013 +0100
     2.3 @@ -179,9 +179,15 @@
     2.4              if Exn.is_interrupt exn then reraise exn
     2.5              else ML_Compiler.exn_messages_ids exn)) ();
     2.6  
     2.7 +fun report tr m =
     2.8 +  Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) ();
     2.9 +
    2.10 +fun status tr m =
    2.11 +  Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
    2.12 +
    2.13  fun proof_status tr st =
    2.14    (case try Toplevel.proof_of st of
    2.15 -    SOME prf => Toplevel.status tr (Proof.status_markup prf)
    2.16 +    SOME prf => status tr (Proof.status_markup prf)
    2.17    | NONE => ());
    2.18  
    2.19  fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
    2.20 @@ -194,7 +200,7 @@
    2.21        val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    2.22  
    2.23        val _ = Multithreading.interrupted ();
    2.24 -      val _ = Toplevel.status tr Markup.running;
    2.25 +      val _ = status tr Markup.running;
    2.26        val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    2.27        val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
    2.28        val errs = errs1 @ errs2;
    2.29 @@ -203,14 +209,14 @@
    2.30        (case result of
    2.31          NONE =>
    2.32            let
    2.33 -            val _ = Toplevel.status tr Markup.failed;
    2.34 -            val _ = Toplevel.status tr Markup.finished;
    2.35 -            val _ = if null errs then Exn.interrupt () else ();
    2.36 +            val _ = status tr Markup.failed;
    2.37 +            val _ = status tr Markup.finished;
    2.38 +            val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
    2.39            in {failed = true, malformed = malformed', command = tr, state = st} end
    2.40        | SOME st' =>
    2.41            let
    2.42              val _ = proof_status tr st';
    2.43 -            val _ = Toplevel.status tr Markup.finished;
    2.44 +            val _ = status tr Markup.finished;
    2.45            in {failed = false, malformed = malformed', command = tr, state = st'} end)
    2.46      end;
    2.47  
     3.1 --- a/src/Pure/PIDE/execution.ML	Thu Dec 05 20:06:28 2013 +0100
     3.2 +++ b/src/Pure/PIDE/execution.ML	Thu Dec 05 20:22:53 2013 +0100
     3.3 @@ -107,13 +107,14 @@
     3.4                val _ = status task [Markup.joined];
     3.5                val _ =
     3.6                  (case result of
     3.7 -                  Exn.Res _ => ()
     3.8 -                | Exn.Exn exn =>
     3.9 +                  Exn.Exn exn =>
    3.10                     (status task [Markup.failed];
    3.11 +                    status task [Markup.finished];
    3.12                      Output.report (Markup.markup_only Markup.bad);
    3.13                      if exec_id = 0 then ()
    3.14 -                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
    3.15 -              val _ = status task [Markup.finished];
    3.16 +                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))
    3.17 +                | Exn.Res _ =>
    3.18 +                    status task [Markup.finished])
    3.19              in Exn.release result end);
    3.20  
    3.21        val _ = status (Future.task_of future) [Markup.forked];