1.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 03 21:55:15 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 03 22:30:33 2013 +0200
     1.3 @@ -17,9 +17,12 @@
     1.4    val read: span -> Toplevel.transition
     1.5    val eval: span -> Toplevel.transition ->
     1.6      Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
     1.7 -  val print: Toplevel.transition -> Toplevel.state -> (string * unit lazy) list
     1.8 -  val print_function: string ->
     1.9 -    ({tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option) -> unit
    1.10 +  type print = {name: string, pri: int, pr: unit lazy}
    1.11 +  val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list
    1.12 +  type print_function =
    1.13 +    {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
    1.14 +      (unit -> unit) option
    1.15 +  val print_function: string -> int -> print_function -> unit
    1.16  end;
    1.17  
    1.18  structure Command: COMMAND =
    1.19 @@ -151,31 +154,35 @@
    1.20  
    1.21  (* print *)
    1.22  
    1.23 +type print_function =
    1.24 +  {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
    1.25 +    (unit -> unit) option;
    1.26 +
    1.27 +type print = {name: string, pri: int, pr: unit lazy};
    1.28 +
    1.29  local
    1.30  
    1.31 -type print_function =
    1.32 -  {tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option;
    1.33 -
    1.34  val print_functions =
    1.35 -  Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
    1.36 +  Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
    1.37  
    1.38  in
    1.39  
    1.40 -fun print tr st' =
    1.41 -  rev (Synchronized.value print_functions) |> map_filter (fn (name, f) =>
    1.42 -    (case f {tr = tr, state = st'} of
    1.43 -      SOME pr => SOME (name, (Lazy.lazy o Toplevel.setmp_thread_position tr) pr)
    1.44 +fun print st tr st' =
    1.45 +  rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
    1.46 +    (case f {old_state = st, tr = tr, state = st'} of
    1.47 +      SOME pr =>
    1.48 +        SOME {name = name, pri = pri, pr = (Lazy.lazy o Toplevel.setmp_thread_position tr) pr}
    1.49      | NONE => NONE));
    1.50  
    1.51 -fun print_function name f =
    1.52 +fun print_function name pri f =
    1.53    Synchronized.change print_functions (fn funs =>
    1.54     (if not (AList.defined (op =) funs name) then ()
    1.55      else warning ("Redefining command print function: " ^ quote name);
    1.56 -    AList.update (op =) (name, f) funs));
    1.57 +    AList.update (op =) (name, (pri, f)) funs));
    1.58  
    1.59  end;
    1.60  
    1.61 -val _ = print_function "print_state" (fn {tr, state} =>
    1.62 +val _ = print_function "print_state" 0 (fn {tr, state, ...} =>
    1.63    let
    1.64      val is_init = Toplevel.is_init tr;
    1.65      val is_proof = Keyword.is_proof (Toplevel.name_of tr);