Command.memo including physical interrupts (unlike Lazy.lazy);
re-assign unstable exec, i.e. reset interrupted transaction;
node result as direct exec -- avoid potential interrupt instability of Lazy.map;

--- a/src/Pure/PIDE/command.ML	Thu Apr 05 10:45:53 2012 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Apr 05 11:58:46 2012 +0200
@@ -7,13 +7,18 @@
 signature COMMAND =
 sig
   val parse_command: string -> string -> Token.T list
+  type 'a memo
+  val memo: (unit -> 'a) -> 'a memo
+  val memo_value: 'a -> 'a memo
+  val memo_result: 'a memo -> 'a Exn.result
+  val memo_stable: 'a memo -> bool
   val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
 end;
 
 structure Command: COMMAND =
 struct
 
-(* parse *)
+(* parse command *)
 
 fun parse_command id text =
   Position.setmp_thread_data (Position.id_only id)
@@ -24,7 +29,37 @@
       in toks end) ();
 
 
-(* run *)
+(* memo results *)
+
+datatype 'a expr =
+  Expr of unit -> 'a |
+  Result of 'a Exn.result;
+
+abstype 'a memo = Memo of 'a expr Synchronized.var
+with
+
+fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
+fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
+
+fun memo_result (Memo v) =
+  (case Synchronized.value v of
+    Result res => res
+  | _ =>
+      Synchronized.guarded_access v
+        (fn Result res => SOME (res, Result res)
+          | Expr e =>
+              let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
+              in SOME (res, Result res) end));
+
+fun memo_stable (Memo v) =
+  (case Synchronized.value v of
+    Result (Exn.Exn exn) => not (Exn.is_interrupt exn)
+  | _ => true);
+
+end;
+
+
+(* run command *)
 
 local
 

--- a/src/Pure/PIDE/document.ML	Thu Apr 05 10:45:53 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Apr 05 11:58:46 2012 +0200
@@ -62,8 +62,8 @@
 type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
-type exec = (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
-val no_exec = (no_id, Lazy.value (Toplevel.toplevel, Lazy.value ()));
+type exec = (Toplevel.state * unit lazy) Command.memo;  (*eval/print process*)
+val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
 
 abstype node = Node of
  {touched: bool,
@@ -71,7 +71,7 @@
   perspective: perspective,
   entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
   last_exec: command_id option,  (*last command with exec state assignment*)
-  result: Toplevel.state lazy}
+  result: exec}
 and version = Version of node Graph.T  (*development graph wrt. static imports*)
 with
 
@@ -87,11 +87,10 @@
 
 val no_header = Exn.Exn (ERROR "Bad theory header");
 val no_perspective = make_perspective [];
-val no_result = Lazy.value Toplevel.toplevel;
 
-val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result);
+val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec);
 val clear_node = map_node (fn (_, header, _, _, _, _) =>
-  (false, header, no_perspective, Entries.empty, NONE, no_result));
+  (false, header, no_perspective, Entries.empty, NONE, no_exec));
 
 
 (* basic components *)
@@ -159,8 +158,8 @@
     NONE => err_undef "command entry" id
   | SOME (exec, _) => exec);
 
-fun the_default_entry node (SOME id) = (id, (the_default no_exec (the_entry node id)))
-  | the_default_entry _ NONE = (no_id, no_exec);
+fun the_default_entry node (SOME id) = (id, (the_default (no_id, no_exec) (the_entry node id)))
+  | the_default_entry _ NONE = (no_id, (no_id, no_exec));
 
 fun update_entry id exec =
   map_entries (Entries.update (id, exec));
@@ -193,7 +192,7 @@
   fold (fn desc =>
       update_node desc
         (set_touched true #>
-          desc <> name ? (map_entries (reset_after NONE) #> set_result no_result)))
+          desc <> name ? (map_entries (reset_after NONE) #> set_result no_exec)))
     (Graph.all_succs nodes [name]) nodes;
 
 in
@@ -338,8 +337,8 @@
           SOME thy => thy
         | NONE =>
             Toplevel.end_theory (Position.file_only import)
-              (Lazy.force
-                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))));
+              (fst (Exn.release (Command.memo_result
+                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))))));
   in Thy_Load.begin_theory master_dir header parents end;
 
 fun check_theory nodes name =
@@ -363,6 +362,7 @@
           (case opt_exec of
             NONE => true
           | SOME (exec_id, exec) =>
+              not (Command.memo_stable exec) orelse
               (case lookup_entry node0 id of
                 NONE => true
               | SOME (exec_id0, _) => exec_id <> exec_id0));
@@ -395,8 +395,9 @@
             #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
             |> modify_init
             |> Toplevel.put_id exec_id'_string);
-      val exec' =
-        snd (snd command_exec) |> Lazy.map (fn (st, _) => Command.run_command (tr ()) st);
+      val exec' = Command.memo (fn () =>
+        let val (st, _) = Exn.release (Command.memo_result (snd (snd command_exec)));
+        in Command.run_command (tr ()) st end);
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;
 
@@ -448,8 +449,8 @@
 
                     val last_exec = if command_id = no_id then NONE else SOME command_id;
                     val result =
-                      if is_some (after_entry node last_exec) then no_result
-                      else Lazy.map #1 exec;
+                      if is_some (after_entry node last_exec) then no_exec
+                      else exec;
 
                     val node' = node
                       |> fold reset_entry no_execs
@@ -485,7 +486,7 @@
       fun force_exec _ _ NONE = ()
         | force_exec node command_id (SOME (_, exec)) =
             let
-              val (_, print) = Lazy.force exec;
+              val (_, print) = Exn.release (Command.memo_result exec);
               val _ =
                 if #1 (get_perspective node) command_id
                 then ignore (Lazy.future Future.default_params print)