more defensive order of Markup.failed vs. Markup.finished -- more informative status in Isabelle/Scala, although it is not rendered in Isabelle/jEdit;
authorwenzelm
Mon Nov 25 21:17:18 2013 +0100 (2013-11-25)
changeset 546477a8512d6206d
parent 54646 2b38549374ba
child 54648 f38b113697a2
more defensive order of Markup.failed vs. Markup.finished -- more informative status in Isabelle/Scala, although it is not rendered in Isabelle/jEdit;
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Mon Nov 25 20:49:20 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Nov 25 21:17:18 2013 +0100
     1.3 @@ -165,18 +165,19 @@
     1.4        val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
     1.5        val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
     1.6        val errs = errs1 @ errs2;
     1.7 -      val _ = Toplevel.status tr Markup.finished;
     1.8        val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
     1.9      in
    1.10        (case result of
    1.11          NONE =>
    1.12            let
    1.13 +            val _ = Toplevel.status tr Markup.failed;
    1.14 +            val _ = Toplevel.status tr Markup.finished;
    1.15              val _ = if null errs then Exn.interrupt () else ();
    1.16 -            val _ = Toplevel.status tr Markup.failed;
    1.17            in {failed = true, malformed = malformed', command = tr, state = st} end
    1.18        | SOME st' =>
    1.19            let
    1.20              val _ = proof_status tr st';
    1.21 +            val _ = Toplevel.status tr Markup.finished;
    1.22            in {failed = false, malformed = malformed', command = tr, state = st'} end)
    1.23      end;
    1.24