1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 05 14:09:06 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 05 15:38:03 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, exec_id: int, print: unit memo}
     1.8 -  val print: (unit -> int) -> string -> eval -> print list
     1.9 +  type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
    1.10 +  val print: 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, exec_id: int, print: unit memo};
    1.19 +type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo};
    1.20  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    1.21  
    1.22  local
    1.23 @@ -192,13 +192,13 @@
    1.24  
    1.25  in
    1.26  
    1.27 -fun print new_id command_name eval =
    1.28 +fun print 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          let
    1.34 -          val exec_id = new_id ();
    1.35 +          val exec_id = Document_ID.make ();
    1.36            fun body () =
    1.37              let
    1.38                val {failed, command, state = st', ...} = memo_result eval;
    1.39 @@ -207,7 +207,7 @@
    1.40          in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
    1.41      | Exn.Exn exn =>
    1.42          let
    1.43 -          val exec_id = new_id ();
    1.44 +          val exec_id = Document_ID.make ();
    1.45            fun body () =
    1.46              let
    1.47                val {command, ...} = memo_result eval;