1.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 10 11:26:55 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 10 11:32:49 2013 +0200
     1.3 @@ -14,14 +14,15 @@
     1.4    type exec = eval * print list
     1.5    val no_exec: exec
     1.6    val exec_ids: exec option -> Document_ID.exec list
     1.7 +  val stable_eval: eval -> bool
     1.8 +  val stable_print: print -> bool
     1.9    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    1.10    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.11    val print: bool -> string -> eval -> print list -> print list option
    1.12    type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.13    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    1.14 +  val no_print_function: string -> unit
    1.15    val execute: exec -> unit
    1.16 -  val stable_eval: eval -> bool
    1.17 -  val stable_print: print -> bool
    1.18  end;
    1.19  
    1.20  structure Command: COMMAND =
    1.21 @@ -259,6 +260,9 @@
    1.22      else warning ("Redefining command print function: " ^ quote name);
    1.23      AList.update (op =) (name, (pri, f)) funs));
    1.24  
    1.25 +fun no_print_function name =
    1.26 +  Synchronized.change print_functions (filter_out (equal name o #1));
    1.27 +
    1.28  end;
    1.29  
    1.30  val _ =