src/Pure/PIDE/command.ML
changeset 48772 e46cd0d26481
parent 48771 2ea997196d04
child 48918 6e5fd4585512
--- a/src/Pure/PIDE/command.ML	Sat Aug 11 18:05:41 2012 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Aug 11 19:34:36 2012 +0200
@@ -13,7 +13,8 @@
   val memo_value: 'a -> 'a memo
   val memo_eval: 'a memo -> 'a
   val memo_result: 'a memo -> 'a
-  val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
+  val run_command: Toplevel.transition ->
+    Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
 end;
 
 structure Command: COMMAND =
@@ -88,34 +89,37 @@
 
 in
 
-fun run_command tr st =
-  let
-    val is_init = Toplevel.is_init tr;
-    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
+fun run_command tr (st, malformed) =
+  if malformed then ((Toplevel.toplevel, malformed), no_print)
+  else
+    let
+      val malformed' = Toplevel.is_malformed tr;
+      val is_init = Toplevel.is_init tr;
+      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
 
-    val _ = Multithreading.interrupted ();
-    val _ = Toplevel.status tr Isabelle_Markup.forked;
-    val start = Timing.start ();
-    val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
-    val _ = timing tr (Timing.result start);
-    val _ = Toplevel.status tr Isabelle_Markup.joined;
-    val _ = List.app (Toplevel.error_msg tr) errs;
-  in
-    (case result of
-      NONE =>
-        let
-          val _ = if null errs then Exn.interrupt () else ();
-          val _ = Toplevel.status tr Isabelle_Markup.failed;
-        in (st, no_print) end
-    | SOME st' =>
-        let
-          val _ = Toplevel.status tr Isabelle_Markup.finished;
-          val _ = proof_status tr st';
-          val do_print =
-            not is_init andalso
-              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
-        in (st', if do_print then print_state tr st' else no_print) end)
-  end;
+      val _ = Multithreading.interrupted ();
+      val _ = Toplevel.status tr Isabelle_Markup.forked;
+      val start = Timing.start ();
+      val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+      val _ = timing tr (Timing.result start);
+      val _ = Toplevel.status tr Isabelle_Markup.joined;
+      val _ = List.app (Toplevel.error_msg tr) errs;
+    in
+      (case result of
+        NONE =>
+          let
+            val _ = if null errs then Exn.interrupt () else ();
+            val _ = Toplevel.status tr Isabelle_Markup.failed;
+          in ((st, malformed'), no_print) end
+      | SOME st' =>
+          let
+            val _ = Toplevel.status tr Isabelle_Markup.finished;
+            val _ = proof_status tr st';
+            val do_print =
+              not is_init andalso
+                (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
+          in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
+    end;
 
 end;