1.1 --- a/src/Pure/PIDE/command.ML	Sat Jul 13 14:13:34 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Sat Jul 13 16:34:57 2013 +0200
     1.3 @@ -15,8 +15,8 @@
     1.4    type print
     1.5    val print: bool -> string -> eval -> print list -> print list option
     1.6    type print_fn = Toplevel.transition -> Toplevel.state -> unit
     1.7 -  val print_function: {name: string, pri: int, persistent: bool} ->
     1.8 -    ({command_name: string} -> print_fn option) -> unit
     1.9 +  val print_function: string ->
    1.10 +    ({command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option) -> unit
    1.11    val no_print_function: string -> unit
    1.12    type exec = eval * print list
    1.13    val no_exec: exec
    1.14 @@ -197,10 +197,13 @@
    1.15  
    1.16  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    1.17  
    1.18 +type print_function =
    1.19 +  {command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option;
    1.20 +
    1.21  local
    1.22  
    1.23 -type print_function = string * (int * bool * ({command_name: string} -> print_fn option));
    1.24 -val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
    1.25 +val print_functions =
    1.26 +  Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
    1.27  
    1.28  fun print_error tr e =
    1.29    (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e ()
    1.30 @@ -219,9 +222,9 @@
    1.31  
    1.32  fun print command_visible command_name eval old_prints =
    1.33    let
    1.34 -    fun new_print (name, (pri, persistent, get_fn)) =
    1.35 +    fun new_print (name, get_pr) =
    1.36        let
    1.37 -        fun make_print strict print_fn =
    1.38 +        fun make_print strict {pri, persistent, print_fn} =
    1.39            let
    1.40              val exec_id = Document_ID.make ();
    1.41              fun process () =
    1.42 @@ -238,10 +241,12 @@
    1.43               exec_id = exec_id, print_process = memo exec_id process}
    1.44            end;
    1.45        in
    1.46 -        (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
    1.47 +        (case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of
    1.48            Exn.Res NONE => NONE
    1.49 -        | Exn.Res (SOME print_fn) => SOME (make_print false print_fn)
    1.50 -        | Exn.Exn exn => SOME (make_print true (fn _ => fn _ => reraise exn)))
    1.51 +        | Exn.Res (SOME pr) => SOME (make_print false pr)
    1.52 +        | Exn.Exn exn =>
    1.53 +            SOME (make_print true
    1.54 +              {pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
    1.55        end;
    1.56  
    1.57      val new_prints =
    1.58 @@ -255,11 +260,11 @@
    1.59      if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
    1.60    end;
    1.61  
    1.62 -fun print_function {name, pri, persistent} f =
    1.63 +fun print_function name f =
    1.64    Synchronized.change print_functions (fn funs =>
    1.65     (if not (AList.defined (op =) funs name) then ()
    1.66      else warning ("Redefining command print function: " ^ quote name);
    1.67 -    AList.update (op =) (name, (pri, persistent, f)) funs));
    1.68 +    AList.update (op =) (name, f) funs));
    1.69  
    1.70  fun no_print_function name =
    1.71    Synchronized.change print_functions (filter_out (equal name o #1));
    1.72 @@ -267,15 +272,15 @@
    1.73  end;
    1.74  
    1.75  val _ =
    1.76 -  print_function {name = "print_state", pri = 0, persistent = true}
    1.77 -    (fn {command_name} => SOME (fn tr => fn st' =>
    1.78 +  print_function "print_state"
    1.79 +    (fn {command_name} => SOME {pri = 0, persistent = true, print_fn = fn tr => fn st' =>
    1.80        let
    1.81          val is_init = Keyword.is_theory_begin command_name;
    1.82          val is_proof = Keyword.is_proof command_name;
    1.83          val do_print =
    1.84            not is_init andalso
    1.85              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.86 -      in if do_print then Toplevel.print_state false st' else () end));
    1.87 +      in if do_print then Toplevel.print_state false st' else () end});
    1.88  
    1.89  
    1.90  (* combined execution *)