1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 04 16:04:53 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 04 23:51:47 2013 +0200
     1.3 @@ -23,8 +23,8 @@
     1.4    val no_eval: eval
     1.5    val eval: span -> Toplevel.transition -> eval_state -> eval_state
     1.6    type print_fn = Toplevel.transition -> Toplevel.state -> unit
     1.7 -  type print = {name: string, pri: int, print: unit memo}
     1.8 -  val print: string -> eval -> print list
     1.9 +  type print = {name: string, pri: int, exec_id: int, print: unit memo}
    1.10 +  val print: (unit -> int) -> string -> eval -> print list
    1.11    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    1.12  end;
    1.13  
    1.14 @@ -175,7 +175,7 @@
    1.15  
    1.16  (* print *)
    1.17  
    1.18 -type print = {name: string, pri: int, print: unit memo};
    1.19 +type print = {name: string, pri: int, exec_id: int, print: unit memo};
    1.20  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    1.21  
    1.22  local
    1.23 @@ -192,18 +192,28 @@
    1.24  
    1.25  in
    1.26  
    1.27 -fun print command_name eval =
    1.28 +fun print new_id command_name eval =
    1.29    rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
    1.30      (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
    1.31        Exn.Res NONE => NONE
    1.32      | Exn.Res (SOME print_fn) =>
    1.33 -        SOME {name = name, pri = pri,
    1.34 -          print = memo (fn () =>
    1.35 -            let val {failed, command = tr, state = st', ...} = memo_result eval
    1.36 -            in if failed then () else print_error tr (fn () => print_fn tr st') () end)}
    1.37 +        let
    1.38 +          val exec_id = new_id ();
    1.39 +          fun body () =
    1.40 +            let
    1.41 +              val {failed, command, state = st', ...} = memo_result eval;
    1.42 +              val tr = Toplevel.put_id exec_id command;
    1.43 +            in if failed then () else print_error tr (fn () => print_fn tr st') () end;
    1.44 +        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
    1.45      | Exn.Exn exn =>
    1.46 -        SOME {name = name, pri = pri,
    1.47 -          print = memo (fn () => output_error (#command (memo_result eval)) exn)}));
    1.48 +        let
    1.49 +          val exec_id = new_id ();
    1.50 +          fun body () =
    1.51 +            let
    1.52 +              val {command, ...} = memo_result eval;
    1.53 +              val tr = Toplevel.put_id exec_id command;
    1.54 +            in output_error tr exn end;
    1.55 +        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
    1.56  
    1.57  fun print_function {name, pri} f =
    1.58    Synchronized.change print_functions (fn funs =>