1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 11 22:53:56 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 11 23:24:40 2013 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    type exec = eval * print list
     1.5    val no_exec: exec
     1.6    val exec_ids: exec option -> Document_ID.exec list
     1.7 -  val exec: exec -> unit
     1.8 +  val exec: Exec.context -> exec -> unit
     1.9  end;
    1.10  
    1.11  structure Command: COMMAND =
    1.12 @@ -43,32 +43,31 @@
    1.13      Result res => Exn.release res
    1.14    | Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
    1.15  
    1.16 -fun memo_exec (Memo v) =
    1.17 +fun memo_exec context (Memo v) =
    1.18    (case Synchronized.value v of
    1.19      Result res => res
    1.20 -  | Expr (exec_id, _) =>
    1.21 +  | Expr _ =>
    1.22        Synchronized.timed_access v (fn _ => SOME Time.zeroTime)
    1.23          (fn Result res => SOME (res, Result res)
    1.24 -          | Expr (exec_id, e) =>
    1.25 +          | expr as Expr (exec_id, e) =>
    1.26                uninterruptible (fn restore_attributes => fn () =>
    1.27 -                let
    1.28 -                  val _ = Exec.running exec_id;
    1.29 -                  val res = Exn.capture (restore_attributes e) ();
    1.30 -                  val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
    1.31 -                in SOME (res, Result res) end) ())
    1.32 -      |> (fn NONE => error ("Concurrent execution attempt: " ^ Document_ID.print exec_id)
    1.33 -           | SOME res => res))
    1.34 -  |> Exn.release;
    1.35 +                if Exec.running context exec_id then
    1.36 +                  let
    1.37 +                    val res = Exn.capture (restore_attributes e) ();
    1.38 +                    val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
    1.39 +                  in SOME (res, Result res) end
    1.40 +                else SOME (Exn.interrupt_exn, expr)) ())
    1.41 +      |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
    1.42 +  |> Exn.release |> ignore;
    1.43  
    1.44 -fun memo_fork params (Memo v) =
    1.45 +fun memo_fork params context (Memo v) =
    1.46    (case Synchronized.value v of
    1.47      Result _ => ()
    1.48 -  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec (Memo v))));
    1.49 +  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec context (Memo v))));
    1.50  
    1.51  end;
    1.52  
    1.53  
    1.54 -
    1.55  (** main phases of execution **)
    1.56  
    1.57  (* read *)
    1.58 @@ -277,15 +276,15 @@
    1.59  
    1.60  local
    1.61  
    1.62 -fun run_print (Print {name, pri, print_process, ...}) =
    1.63 +fun run_print context (Print {name, pri, print_process, ...}) =
    1.64    (if Multithreading.enabled () then
    1.65      memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
    1.66 -  else memo_exec) print_process;
    1.67 +  else memo_exec) context print_process;
    1.68  
    1.69  in
    1.70  
    1.71 -fun exec (Eval {eval_process, ...}, prints) =
    1.72 -  (memo_exec eval_process; List.app run_print prints);
    1.73 +fun exec context (Eval {eval_process, ...}, prints) =
    1.74 +  (memo_exec context eval_process; List.app (run_print context) prints);
    1.75  
    1.76  end;
    1.77