# HG changeset patch
# User wenzelm
# Date 1256639156 -3600
# Node ID 11a1af478dac0fd69ad00ba672de0ed977c83524
# Parent  a69147d95957d5cec1b89e3ca38e00736a80ec1d
SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;

diff -r a69147d95957 -r 11a1af478dac src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Oct 27 10:54:25 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Oct 27 11:25:56 2009 +0100
@@ -271,7 +271,7 @@
                     Markup.markup Markup.sendback "apply metis")
                 | ERROR msg => (false, "Error: " ^ msg);
             val _ = unregister result (Thread.self ());
-          in () end handle Exn.Interrupt => ())
+          in () end)
       in () end);
 
 
diff -r a69147d95957 -r 11a1af478dac src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 10:54:25 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 11:25:56 2009 +0100
@@ -432,7 +432,7 @@
     if auto orelse blocking then
       go ()
     else
-      (SimpleThread.fork true (fn () => (go (); ()) handle Exn.Interrupt => ());
+      (SimpleThread.fork true (fn () => (go (); ()));
        state)
   end
 
diff -r a69147d95957 -r 11a1af478dac src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Tue Oct 27 10:54:25 2009 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML	Tue Oct 27 11:25:56 2009 +0100
@@ -15,7 +15,7 @@
 struct
 
 fun fork interrupts body =
-  Thread.fork (fn () => exception_trace (fn () => body ()),
+  Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
     if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
 
 fun interrupt thread = Thread.interrupt thread handle Thread _ => ();