# HG changeset patch
# User wenzelm
# Date 1289073599 -3600
# Node ID cdda2847a91e3f0398c050b3c621d2d652de7a91
# Parent  4ad71312a192ef7f2cd51e1fe48c9e5674eed8c8
continue after failed commands;

diff -r 4ad71312a192 -r cdda2847a91e src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Nov 06 20:18:06 2010 +0100
+++ b/src/Pure/PIDE/document.ML	Sat Nov 06 20:59:59 2010 +0100
@@ -119,10 +119,10 @@
 (** global state -- document structure and execution process **)
 
 abstype state = State of
- {versions: version Inttab.table,                     (*version_id -> document content*)
+ {versions: version Inttab.table,  (*version_id -> document content*)
   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
-  execs: Toplevel.state option lazy Inttab.table,     (*exec_id -> execution process*)
-  execution: unit future list}                        (*global execution process*)
+  execs: (bool * Toplevel.state) lazy Inttab.table,  (*exec_id -> execution process*)
+  execution: unit future list}  (*global execution process*)
 with
 
 fun make_state (versions, commands, execs, execution) =
@@ -134,7 +134,7 @@
 val init_state =
   make_state (Inttab.make [(no_id, empty_version)],
     Inttab.make [(no_id, Future.value Toplevel.empty)],
-    Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],
+    Inttab.make [(no_id, Lazy.value (true, Toplevel.toplevel))],
     []);
 
 
@@ -235,19 +235,21 @@
         val (errs, result) = run int tr st;
         val _ = timing tr (end_timing start);
         val _ = List.app (Toplevel.error_msg tr) errs;
-        val _ =
+        val res =
           (case result of
-            NONE => Toplevel.status tr Markup.failed
+            NONE => (Toplevel.status tr Markup.failed; (false, st))
           | SOME st' =>
              (Toplevel.status tr Markup.finished;
               proof_status tr st';
-              if int then () else async_state tr st'));
-      in result end
+              if int then () else async_state tr st';
+              (true, st')));
+      in res end
   | Exn.Exn exn =>
       if Exn.is_interrupt exn then reraise exn
       else
        (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
-        Toplevel.status tr Markup.failed; NONE));
+        Toplevel.status tr Markup.failed;
+        (false, Toplevel.toplevel)));
 
 end;
 
@@ -272,11 +274,10 @@
     val future_tr = the_command state id;
     val exec' =
       Lazy.lazy (fn () =>
-        (case Lazy.force exec of
-          NONE => NONE
-        | SOME st =>
-            let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
-            in run_command name exec_tr st end));
+        let
+          val st = #2 (Lazy.force exec);
+          val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
+        in run_command name exec_tr st end);
     val state' = define_exec exec_id' exec' state;
   in (exec_id', (id, exec_id') :: updates, state') end;