avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);
authorwenzelm
Tue, 24 Sep 2013 13:23:25 +0200
changeset 53839 274a892b1230
parent 53838 b9285f30a80a
child 53840 75243ba102d4
avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);
src/Tools/try.ML
--- a/src/Tools/try.ML	Tue Sep 24 11:28:18 2013 +0200
+++ b/src/Tools/try.ML	Tue Sep 24 13:23:25 2013 +0200
@@ -116,7 +116,7 @@
 (* asynchronous print function (PIDE) *)
 
 fun print_function ((name, (weight, auto, tool)): tool) =
-  Command.print_function name
+  Command.print_function ("auto_" ^ name)
     (fn {command_name, ...} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
         SOME