# HG changeset patch
# User wenzelm
# Date 1373726747 -7200
# Node ID b1ae4306f29f5499460361fe2e5aaf5e9f8f7534
# Parent  45ce95b8bf6956f610d594fd8c37bfc1102fcd79
tuned;

diff -r 45ce95b8bf69 -r b1ae4306f29f src/Tools/try.ML
--- a/src/Tools/try.ML	Sat Jul 13 16:34:57 2013 +0200
+++ b/src/Tools/try.ML	Sat Jul 13 16:45:47 2013 +0200
@@ -121,26 +121,22 @@
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
         SOME {pri = ~ weight, persistent = true, print_fn = fn _ => fn st =>
           let
+            val state = Toplevel.proof_of st
             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 state =>
-                  (case
-                    (try o TimeLimit.timeLimit (seconds auto_time_limit))
-                      (fn () => tool true state) () of
-                    SOME (true, (_, state')) =>
-                      List.app Pretty.writeln (Proof.pretty_goal_messages state')
-                  | _ => ())
-              | NONE => ())
+              (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
+                (true, (_, state')) =>
+                  List.app Pretty.writeln (Proof.pretty_goal_messages state')
+              | _ => ())
             else ()
-          end}
-      else NONE);
+          end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
+      else NONE)
 
 
 (* hybrid tool setup *)
 
 fun tool_setup tool =
-  (Context.>> (Context.map_theory (register_tool tool)); print_function tool);
+  (Context.>> (Context.map_theory (register_tool tool)); print_function tool)
 
 end;