# HG changeset patch
# User wenzelm
# Date 1203176639 -3600
# Node ID fbdb1161b4b0b6ad3934172ba80415f584391cba
# Parent  d920e4c8ba82f310f1f769571dac5bd1cdb49caf
exn_message: added TimeLimit.TimeOut;
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;

diff -r d920e4c8ba82 -r fbdb1161b4b0 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Feb 16 16:43:57 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Feb 16 16:43:59 2008 +0100
@@ -262,6 +262,7 @@
 fun exn_msg _ TERMINATE = "Exit."
   | exn_msg _ RESTART = "Restart."
   | exn_msg _ Interrupt = "Interrupt."
+  | exn_msg _ TimeLimit.TimeOut = "Timeout."
   | exn_msg _ TOPLEVEL_ERROR = "Error."
   | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
   | exn_msg _ (ERROR msg) = msg
@@ -305,10 +306,6 @@
   if ! debug then exception_trace (fn () => f x)
   else f x;
 
-fun interruptible f x =
-  let val y = ref NONE
-  in raise_interrupt (fn () => y := SOME (f x)) (); the (! y) end;
-
 fun toplevel_error f x = f x
   handle exn => (Output.error_msg (exn_message exn); raise TOPLEVEL_ERROR);
 
@@ -771,7 +768,7 @@
 
 in
 
-fun loop secure src = ignore_interrupt (raw_loop secure) src;
+fun loop secure src = uninterruptible (fn _ => raw_loop secure) src;
 
 end;