1.1 --- a/src/Pure/PIDE/command.ML	Fri Aug 02 14:26:09 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Aug 02 16:00:14 2013 +0200
     1.3 @@ -14,10 +14,11 @@
     1.4    val eval_result_state: eval -> Toplevel.state
     1.5    val eval: (unit -> theory) -> Token.T list -> eval -> eval
     1.6    type print
     1.7 -  val print: bool -> string -> eval -> print list -> print list option
     1.8 +  val print: bool -> (string * string list) list -> string ->
     1.9 +    eval -> print list -> print list option
    1.10    type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.11    val print_function: string ->
    1.12 -    ({command_name: string} ->
    1.13 +    ({command_name: string, args: string list} ->
    1.14        {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
    1.15    val no_print_function: string -> unit
    1.16    type exec = eval * print list
    1.17 @@ -195,13 +196,13 @@
    1.18  (* print *)
    1.19  
    1.20  datatype print = Print of
    1.21 - {name: string, delay: Time.time option, pri: int, persistent: bool,
    1.22 + {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
    1.23    exec_id: Document_ID.exec, print_process: unit memo};
    1.24  
    1.25  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    1.26  
    1.27  type print_function =
    1.28 -  {command_name: string} ->
    1.29 +  {command_name: string, args: string list} ->
    1.30      {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
    1.31  
    1.32  local
    1.33 @@ -223,9 +224,11 @@
    1.34  
    1.35  in
    1.36  
    1.37 -fun print command_visible command_name eval old_prints =
    1.38 +fun print command_visible command_overlays command_name eval old_prints =
    1.39    let
    1.40 -    fun new_print (name, get_pr) =
    1.41 +    val print_functions = Synchronized.value print_functions;
    1.42 +
    1.43 +    fun new_print name args get_pr =
    1.44        let
    1.45          fun make_print strict {delay, pri, persistent, print_fn} =
    1.46            let
    1.47 @@ -240,11 +243,12 @@
    1.48                end;
    1.49            in
    1.50             Print {
    1.51 -             name = name, delay = delay, pri = pri, persistent = persistent,
    1.52 +             name = name, args = args, delay = delay, pri = pri, persistent = persistent,
    1.53               exec_id = exec_id, print_process = memo exec_id process}
    1.54            end;
    1.55 +        val params = {command_name = command_name, args = args};
    1.56        in
    1.57 -        (case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of
    1.58 +        (case Exn.capture (Runtime.controlled_execution get_pr) params of
    1.59            Exn.Res NONE => NONE
    1.60          | Exn.Res (SOME pr) => SOME (make_print false pr)
    1.61          | Exn.Exn exn =>
    1.62 @@ -252,12 +256,18 @@
    1.63                {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
    1.64        end;
    1.65  
    1.66 +    fun get_print (a, b) =
    1.67 +      (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
    1.68 +        NONE =>
    1.69 +          (case AList.lookup (op =) print_functions a of
    1.70 +            NONE => NONE
    1.71 +          | SOME get_pr => new_print a b get_pr)
    1.72 +      | some => some);
    1.73 +
    1.74      val new_prints =
    1.75        if command_visible then
    1.76 -        rev (Synchronized.value print_functions) |> map_filter (fn pr =>
    1.77 -          (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
    1.78 -            NONE => new_print pr
    1.79 -          | some => some))
    1.80 +        distinct (op =) (fold (fn (a, _) => cons (a, [])) print_functions command_overlays)
    1.81 +        |> map_filter get_print
    1.82        else filter (fn print => print_finished print andalso print_persistent print) old_prints;
    1.83    in
    1.84      if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
    1.85 @@ -276,7 +286,7 @@
    1.86  
    1.87  val _ =
    1.88    print_function "print_state"
    1.89 -    (fn {command_name} =>
    1.90 +    (fn {command_name, ...} =>
    1.91        SOME {delay = NONE, pri = 1, persistent = true,
    1.92          print_fn = fn tr => fn st' =>
    1.93            let