src/Tools/try.ML

 
 
 (* asynchronous print function (PIDE) *)
 
 fun print_function ((name, (weight, auto, tool)): tool) =
-  Command.print_function {name = name, pri = ~ weight, persistent = true}
+  Command.print_function name
     (fn {command_name} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
-        SOME (fn _ => fn st =>
+        SOME {pri = ~ weight, persistent = true, print_fn = fn _ => fn st =>
           let
             val auto_time_limit = Options.default_real @{option auto_time_limit}
           in
             if auto_time_limit > 0.0 then
               (case try Toplevel.proof_of st of

                     SOME (true, (_, state')) =>
                       List.app Pretty.writeln (Proof.pretty_goal_messages state')
                   | _ => ())
               | NONE => ())
             else ()
-          end)
+          end}
       else NONE);
 
 
 (* hybrid tool setup *)