diff -r 9bbf7fd96bcd -r 00f6279bb67a src/Pure/PIDE/command.ML
--- 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