1.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 10 11:32:49 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 10 12:10:32 2013 +0200
     1.3 @@ -10,7 +10,9 @@
     1.4    type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
     1.5    val eval_result_state: eval -> Toplevel.state
     1.6    type print_process
     1.7 -  type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
     1.8 +  type print =
     1.9 +   {name: string, pri: int, persistent: bool,
    1.10 +    exec_id: Document_ID.exec, print_process: print_process}
    1.11    type exec = eval * print list
    1.12    val no_exec: exec
    1.13    val exec_ids: exec option -> Document_ID.exec list
    1.14 @@ -20,7 +22,8 @@
    1.15    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.16    val print: bool -> string -> eval -> print list -> print list option
    1.17    type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.18 -  val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    1.19 +  val print_function: {name: string, pri: int, persistent: bool} ->
    1.20 +    ({command_name: string} -> print_fn option) -> unit
    1.21    val no_print_function: string -> unit
    1.22    val execute: exec -> unit
    1.23  end;
    1.24 @@ -86,7 +89,9 @@
    1.25  val eval_result_state = #state o eval_result;
    1.26  
    1.27  type print_process = unit memo;
    1.28 -type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
    1.29 +type print =
    1.30 + {name: string, pri: int, persistent: bool,
    1.31 +  exec_id: Document_ID.exec, print_process: print_process};
    1.32  
    1.33  type exec = eval * print list;
    1.34  val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
    1.35 @@ -210,7 +215,7 @@
    1.36  
    1.37  local
    1.38  
    1.39 -type print_function = string * (int * (string -> print_fn option));
    1.40 +type print_function = string * (int * bool * ({command_name: string} -> print_fn option));
    1.41  val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
    1.42  
    1.43  fun print_error tr e =
    1.44 @@ -221,7 +226,7 @@
    1.45  
    1.46  fun print command_visible command_name eval old_prints =
    1.47    let
    1.48 -    fun new_print (name, (pri, get_print_fn)) =
    1.49 +    fun new_print (name, (pri, persistent, get_fn)) =
    1.50        let
    1.51          fun make_print strict print_fn =
    1.52            let
    1.53 @@ -234,9 +239,12 @@
    1.54                  if failed andalso not strict then ()
    1.55                  else print_error tr (fn () => print_fn tr st')
    1.56                end;
    1.57 -          in {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end;
    1.58 +          in
    1.59 +           {name = name, pri = pri, persistent = persistent,
    1.60 +            exec_id = exec_id, print_process = memo process}
    1.61 +          end;
    1.62        in
    1.63 -        (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
    1.64 +        (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
    1.65            Exn.Res NONE => NONE
    1.66          | Exn.Res (SOME print_fn) => SOME (make_print false print_fn)
    1.67          | Exn.Exn exn => SOME (make_print true (fn _ => fn _ => reraise exn)))
    1.68 @@ -248,17 +256,17 @@
    1.69            (case find_first (equal (fst pr) o #name) old_prints of
    1.70              SOME print => if stable_print print then SOME print else new_print pr
    1.71            | NONE => new_print pr))
    1.72 -      else filter stable_print old_prints;
    1.73 +      else filter (fn print => #persistent print andalso stable_print print) old_prints;
    1.74    in
    1.75      if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE
    1.76      else SOME new_prints
    1.77    end;
    1.78  
    1.79 -fun print_function {name, pri} f =
    1.80 +fun print_function {name, pri, persistent} f =
    1.81    Synchronized.change print_functions (fn funs =>
    1.82     (if not (AList.defined (op =) funs name) then ()
    1.83      else warning ("Redefining command print function: " ^ quote name);
    1.84 -    AList.update (op =) (name, (pri, f)) funs));
    1.85 +    AList.update (op =) (name, (pri, persistent, f)) funs));
    1.86  
    1.87  fun no_print_function name =
    1.88    Synchronized.change print_functions (filter_out (equal name o #1));
    1.89 @@ -266,14 +274,15 @@
    1.90  end;
    1.91  
    1.92  val _ =
    1.93 -  print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
    1.94 -    let
    1.95 -      val is_init = Keyword.is_theory_begin command_name;
    1.96 -      val is_proof = Keyword.is_proof command_name;
    1.97 -      val do_print =
    1.98 -        not is_init andalso
    1.99 -          (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   1.100 -    in if do_print then Toplevel.print_state false st' else () end));
   1.101 +  print_function {name = "print_state", pri = 0, persistent = true}
   1.102 +    (fn {command_name} => SOME (fn tr => fn st' =>
   1.103 +      let
   1.104 +        val is_init = Keyword.is_theory_begin command_name;
   1.105 +        val is_proof = Keyword.is_proof command_name;
   1.106 +        val do_print =
   1.107 +          not is_init andalso
   1.108 +            (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   1.109 +      in if do_print then Toplevel.print_state false st' else () end));
   1.110  
   1.111  
   1.112  (* overall execution process *)