src/Pure/PIDE/command.ML

--- a/src/Pure/PIDE/command.ML	Wed Jul 10 11:26:55 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Jul 10 11:32:49 2013 +0200
@@ -14,14 +14,15 @@
   type exec = eval * print list
   val no_exec: exec
   val exec_ids: exec option -> Document_ID.exec list
+  val stable_eval: eval -> bool
+  val stable_print: print -> bool
   val read: (unit -> theory) -> Token.T list -> Toplevel.transition
   val eval: (unit -> theory) -> Token.T list -> eval -> eval
   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} -> (string -> print_fn option) -> unit
+  val no_print_function: string -> unit
   val execute: exec -> unit
-  val stable_eval: eval -> bool
-  val stable_print: print -> bool
 end;
 
 structure Command: COMMAND =
@@ -259,6 +260,9 @@
     else warning ("Redefining command print function: " ^ quote name);
     AList.update (op =) (name, (pri, f)) funs));
 
+fun no_print_function name =
+  Synchronized.change print_functions (filter_out (equal name o #1));
+
 end;
 
 val _ =