# 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 _ =