src/Pure/PIDE/command.ML
changeset 48772 e46cd0d26481
parent 48771 2ea997196d04
child 48918 6e5fd4585512
     1.1 --- a/src/Pure/PIDE/command.ML	Sat Aug 11 18:05:41 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Sat Aug 11 19:34:36 2012 +0200
     1.3 @@ -13,7 +13,8 @@
     1.4    val memo_value: 'a -> 'a memo
     1.5    val memo_eval: 'a memo -> 'a
     1.6    val memo_result: 'a memo -> 'a
     1.7 -  val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
     1.8 +  val run_command: Toplevel.transition ->
     1.9 +    Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
    1.10  end;
    1.11  
    1.12  structure Command: COMMAND =
    1.13 @@ -88,34 +89,37 @@
    1.14  
    1.15  in
    1.16  
    1.17 -fun run_command tr st =
    1.18 -  let
    1.19 -    val is_init = Toplevel.is_init tr;
    1.20 -    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    1.21 +fun run_command tr (st, malformed) =
    1.22 +  if malformed then ((Toplevel.toplevel, malformed), no_print)
    1.23 +  else
    1.24 +    let
    1.25 +      val malformed' = Toplevel.is_malformed tr;
    1.26 +      val is_init = Toplevel.is_init tr;
    1.27 +      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    1.28  
    1.29 -    val _ = Multithreading.interrupted ();
    1.30 -    val _ = Toplevel.status tr Isabelle_Markup.forked;
    1.31 -    val start = Timing.start ();
    1.32 -    val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    1.33 -    val _ = timing tr (Timing.result start);
    1.34 -    val _ = Toplevel.status tr Isabelle_Markup.joined;
    1.35 -    val _ = List.app (Toplevel.error_msg tr) errs;
    1.36 -  in
    1.37 -    (case result of
    1.38 -      NONE =>
    1.39 -        let
    1.40 -          val _ = if null errs then Exn.interrupt () else ();
    1.41 -          val _ = Toplevel.status tr Isabelle_Markup.failed;
    1.42 -        in (st, no_print) end
    1.43 -    | SOME st' =>
    1.44 -        let
    1.45 -          val _ = Toplevel.status tr Isabelle_Markup.finished;
    1.46 -          val _ = proof_status tr st';
    1.47 -          val do_print =
    1.48 -            not is_init andalso
    1.49 -              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.50 -        in (st', if do_print then print_state tr st' else no_print) end)
    1.51 -  end;
    1.52 +      val _ = Multithreading.interrupted ();
    1.53 +      val _ = Toplevel.status tr Isabelle_Markup.forked;
    1.54 +      val start = Timing.start ();
    1.55 +      val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    1.56 +      val _ = timing tr (Timing.result start);
    1.57 +      val _ = Toplevel.status tr Isabelle_Markup.joined;
    1.58 +      val _ = List.app (Toplevel.error_msg tr) errs;
    1.59 +    in
    1.60 +      (case result of
    1.61 +        NONE =>
    1.62 +          let
    1.63 +            val _ = if null errs then Exn.interrupt () else ();
    1.64 +            val _ = Toplevel.status tr Isabelle_Markup.failed;
    1.65 +          in ((st, malformed'), no_print) end
    1.66 +      | SOME st' =>
    1.67 +          let
    1.68 +            val _ = Toplevel.status tr Isabelle_Markup.finished;
    1.69 +            val _ = proof_status tr st';
    1.70 +            val do_print =
    1.71 +              not is_init andalso
    1.72 +                (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.73 +          in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
    1.74 +    end;
    1.75  
    1.76  end;
    1.77