determine print function parameters dynamically, e.g. depending on runtime options;

--- a/src/Pure/PIDE/command.ML	Sat Jul 13 14:13:34 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Jul 13 16:34:57 2013 +0200
@@ -15,8 +15,8 @@
   type print
   val print: bool -> string -> eval -> print list -> print list option
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
-  val print_function: {name: string, pri: int, persistent: bool} ->
-    ({command_name: string} -> print_fn option) -> unit
+  val print_function: string ->
+    ({command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option) -> unit
   val no_print_function: string -> unit
   type exec = eval * print list
   val no_exec: exec
@@ -197,10 +197,13 @@
 
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
+type print_function =
+  {command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option;
+
 local
 
-type print_function = string * (int * bool * ({command_name: string} -> print_fn option));
-val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
+val print_functions =
+  Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
 fun print_error tr e =
   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e ()
@@ -219,9 +222,9 @@
 
 fun print command_visible command_name eval old_prints =
   let
-    fun new_print (name, (pri, persistent, get_fn)) =
+    fun new_print (name, get_pr) =
       let
-        fun make_print strict print_fn =
+        fun make_print strict {pri, persistent, print_fn} =
           let
             val exec_id = Document_ID.make ();
             fun process () =
@@ -238,10 +241,12 @@
              exec_id = exec_id, print_process = memo exec_id process}
           end;
       in
-        (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
+        (case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of
           Exn.Res NONE => NONE
-        | Exn.Res (SOME print_fn) => SOME (make_print false print_fn)
-        | Exn.Exn exn => SOME (make_print true (fn _ => fn _ => reraise exn)))
+        | Exn.Res (SOME pr) => SOME (make_print false pr)
+        | Exn.Exn exn =>
+            SOME (make_print true
+              {pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
       end;
 
     val new_prints =
@@ -255,11 +260,11 @@
     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   end;
 
-fun print_function {name, pri, persistent} f =
+fun print_function name f =
   Synchronized.change print_functions (fn funs =>
    (if not (AList.defined (op =) funs name) then ()
     else warning ("Redefining command print function: " ^ quote name);
-    AList.update (op =) (name, (pri, persistent, f)) funs));
+    AList.update (op =) (name, f) funs));
 
 fun no_print_function name =
   Synchronized.change print_functions (filter_out (equal name o #1));
@@ -267,15 +272,15 @@
 end;
 
 val _ =
-  print_function {name = "print_state", pri = 0, persistent = true}
-    (fn {command_name} => SOME (fn tr => fn st' =>
+  print_function "print_state"
+    (fn {command_name} => SOME {pri = 0, persistent = true, print_fn = fn tr => fn st' =>
       let
         val is_init = Keyword.is_theory_begin command_name;
         val is_proof = Keyword.is_proof command_name;
         val do_print =
           not is_init andalso
             (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
-      in if do_print then Toplevel.print_state false st' else () end));
+      in if do_print then Toplevel.print_state false st' else () end});
 
 
 (* combined execution *)

--- a/src/Tools/try.ML	Sat Jul 13 14:13:34 2013 +0200
+++ b/src/Tools/try.ML	Sat Jul 13 16:34:57 2013 +0200
@@ -116,10 +116,10 @@
 (* asynchronous print function (PIDE) *)
 
 fun print_function ((name, (weight, auto, tool)): tool) =
-  Command.print_function {name = name, pri = ~ weight, persistent = true}
+  Command.print_function name
     (fn {command_name} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
-        SOME (fn _ => fn st =>
+        SOME {pri = ~ weight, persistent = true, print_fn = fn _ => fn st =>
           let
             val auto_time_limit = Options.default_real @{option auto_time_limit}
           in
@@ -134,7 +134,7 @@
                   | _ => ())
               | NONE => ())
             else ()
-          end)
+          end}
       else NONE);