1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 29 16:52:04 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 29 18:59:58 2013 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  structure Command: COMMAND =
     1.5  struct
     1.6  
     1.7 -(** memo results -- including physical interrupts **)
     1.8 +(** memo results **)
     1.9  
    1.10  datatype 'a expr =
    1.11    Expr of Document_ID.exec * (unit -> 'a) |
    1.12 @@ -48,24 +48,25 @@
    1.13  fun memo_finished (Memo v) =
    1.14    (case Synchronized.value v of
    1.15     Expr _ => false
    1.16 - | Result res => not (Exn.is_interrupt_exn res));
    1.17 + | Result _ => true);
    1.18  
    1.19  fun memo_exec execution_id (Memo v) =
    1.20    Synchronized.timed_access v (K (SOME Time.zeroTime))
    1.21      (fn expr =>
    1.22        (case expr of
    1.23 -        Expr (exec_id, e) =>
    1.24 +        Expr (exec_id, body) =>
    1.25            uninterruptible (fn restore_attributes => fn () =>
    1.26              if Execution.running execution_id exec_id then
    1.27                let
    1.28 -                val res = Exn.capture (restore_attributes e) ();
    1.29 -                val _ = Execution.finished exec_id;
    1.30 -              in SOME (Exn.is_interrupt_exn res, Result res) end
    1.31 -            else SOME (true, expr)) ()
    1.32 -      | Result _ => SOME (false, expr)))
    1.33 -  |> (fn SOME false => ()
    1.34 -       | SOME true => Exn.interrupt ()
    1.35 -       | NONE => error "Conflicting command execution");
    1.36 +                val res =
    1.37 +                  (body
    1.38 +                    |> restore_attributes
    1.39 +                    |> Future.worker_nest "Command.memo_exec"
    1.40 +                    |> Exn.interruptible_capture) ();
    1.41 +              in SOME ((), Result res) end
    1.42 +            else SOME ((), expr)) ()
    1.43 +      | Result _ => SOME ((), expr)))
    1.44 +  |> (fn NONE => error "Conflicting command execution" | _ => ());
    1.45  
    1.46  fun memo_fork params execution_id (Memo v) =
    1.47    (case Synchronized.value v of
    1.48 @@ -216,7 +217,7 @@
    1.49  
    1.50  fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.51  
    1.52 -fun print_finished (Print {exec_id, print_process, ...}) = memo_finished print_process;
    1.53 +fun print_finished (Print {print_process, ...}) = memo_finished print_process;
    1.54  
    1.55  fun print_persistent (Print {persistent, ...}) = persistent;
    1.56