# HG changeset patch
# User wenzelm
# Date 1288296240 -7200
# Node ID 87998864284eb6b326c60e9853e3d8bd66a9dbb7
# Parent  39af96cc57cbf77f7a1e26cd0284158b087d44d4
use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);

diff -r 39af96cc57cb -r 87998864284e src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Thu Oct 28 21:59:01 2010 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Thu Oct 28 22:04:00 2010 +0200
@@ -547,7 +547,7 @@
     fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
       | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
 
-    val exn_results = map (Exn.capture ast_of) pts;
+    val exn_results = map (Exn.interruptible_capture ast_of) pts;
     val exns = map_filter Exn.get_exn exn_results;
     val results = map_filter Exn.get_result exn_results
   in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
@@ -571,7 +571,7 @@
           Term.list_comb (term_of ast, map term_of asts)
       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
 
-    val exn_results = map (Exn.capture term_of) asts;
+    val exn_results = map (Exn.interruptible_capture term_of) asts;
     val exns = map_filter Exn.get_exn exn_results;
     val results = map_filter Exn.get_result exn_results
   in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
diff -r 39af96cc57cb -r 87998864284e src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Oct 28 21:59:01 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu Oct 28 22:04:00 2010 +0200
@@ -105,7 +105,7 @@
     val (program_code, [SOME value_name']) = serializer naming program' [value_name];
     val value_code = space_implode " "
       (value_name' :: "()" :: map (enclose "(" ")") args);
-  in Exn.capture (value ctxt cookie) (program_code, value_code) end;
+  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
 
 fun partiality_as_none e = SOME (Exn.release e)
   handle General.Match => NONE
diff -r 39af96cc57cb -r 87998864284e src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Oct 28 21:59:01 2010 +0200
+++ b/src/Tools/quickcheck.ML	Thu Oct 28 22:04:00 2010 +0200
@@ -139,9 +139,10 @@
 
 fun mk_testers_strict ctxt t =
   let
-    val generators = ((map snd o fst o Data.get  o Context.Proof) ctxt)
-    val testers = map (fn generator => Exn.capture (generator ctxt) t) generators;
-  in if forall (is_none o Exn.get_result) testers
+    val generators = ((map snd o fst o Data.get o Context.Proof) ctxt)
+    val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators;
+  in
+    if forall (is_none o Exn.get_result) testers
     then [(Exn.release o snd o split_last) testers]
     else map_filter Exn.get_result testers
   end;