src/Pure/PIDE/command.ML

   val eval_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
   val eval: (unit -> theory) -> Token.T list -> eval -> eval
   type print
-  val print: bool -> string -> eval -> print list -> print list option
+  val print: bool -> (string * string list) list -> string ->
+    eval -> print list -> print list option
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   val print_function: string ->
-    ({command_name: string} ->
+    ({command_name: string, args: string list} ->
       {delay: Time.time option, 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
   val exec_ids: exec option -> Document_ID.exec list

 
 
 (* print *)
 
 datatype print = Print of
- {name: string, delay: Time.time option, pri: int, persistent: bool,
+ {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
   exec_id: Document_ID.exec, print_process: unit memo};
 
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 type print_function =
-  {command_name: string} ->
+  {command_name: string, args: string list} ->
     {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
 
 local
 
 val print_functions =

 
 fun print_persistent (Print {persistent, ...}) = persistent;
 
 in
 
-fun print command_visible command_name eval old_prints =
+fun print command_visible command_overlays command_name eval old_prints =
   let
-    fun new_print (name, get_pr) =
+    val print_functions = Synchronized.value print_functions;
+
+    fun new_print name args get_pr =
       let
         fun make_print strict {delay, pri, persistent, print_fn} =
           let
             val exec_id = Document_ID.make ();
             fun process () =

                 if failed andalso not strict then ()
                 else print_error tr (fn () => print_fn tr st')
               end;
           in
            Print {
-             name = name, delay = delay, pri = pri, persistent = persistent,
+             name = name, args = args, delay = delay, pri = pri, persistent = persistent,
              exec_id = exec_id, print_process = memo exec_id process}
           end;
+        val params = {command_name = command_name, args = args};
       in
-        (case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of
+        (case Exn.capture (Runtime.controlled_execution get_pr) params of
           Exn.Res NONE => NONE
         | Exn.Res (SOME pr) => SOME (make_print false pr)
         | Exn.Exn exn =>
             SOME (make_print true
               {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
       end;
 
+    fun get_print (a, b) =
+      (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
+        NONE =>
+          (case AList.lookup (op =) print_functions a of
+            NONE => NONE
+          | SOME get_pr => new_print a b get_pr)
+      | some => some);
+
     val new_prints =
       if command_visible then
-        rev (Synchronized.value print_functions) |> map_filter (fn pr =>
-          (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
-            NONE => new_print pr
-          | some => some))
+        distinct (op =) (fold (fn (a, _) => cons (a, [])) print_functions command_overlays)
+        |> map_filter get_print
       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   in
     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   end;
 

 
 end;
 
 val _ =
   print_function "print_state"
-    (fn {command_name} =>
+    (fn {command_name, ...} =>
       SOME {delay = NONE, pri = 1, 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;