# HG changeset patch
# User wenzelm
# Date 1373448769 -7200
# Node ID 344527354323c50a544f3eabc3cef57653b9152f
# Parent  26d84a0b92090824c18870d5c11b45a003ef4b39
allow to remove print functions;
tuned signature;

diff -r 26d84a0b9209 -r 344527354323 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 _ =