# HG changeset patch
# User wenzelm
# Date 1185299075 -7200
# Node ID c2ee97a963db65598fb82c17fc4e7fb8b30d9c99
# Parent  e0358fac0541b3b039ed64588b63fade3fe0b182
moved exception capture/release to structure Exn;

diff -r e0358fac0541 -r c2ee97a963db src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Jul 24 19:44:33 2007 +0200
+++ b/src/Pure/General/output.ML	Tue Jul 24 19:44:35 2007 +0200
@@ -191,7 +191,7 @@
       Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
     val {name, timer, sys, usr, gc, count} = time_check ti;
     val (sys1, usr1, gc1) = check_timer timer;
-    val result = capture f x;
+    val result = Exn.capture f x;
     val (sys2, usr2, gc2) = check_timer timer;
   in
     ti := TI
@@ -201,7 +201,7 @@
       usr = add_diff usr usr1 usr2,
       gc = add_diff gc gc1 gc2,
       count = count + 1};
-    release result
+    Exn.release result
   end;
 
 fun time_finish ti =
diff -r e0358fac0541 -r c2ee97a963db src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jul 24 19:44:33 2007 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 24 19:44:35 2007 +0200
@@ -929,7 +929,7 @@
       (Seq.pull oo local_skip_proof) true
       |> setmp testing true
       |> setmp proofs 0
-      |> capture;
+      |> Exn.capture;
 
     fun after_qed' results =
       refine_goals print_rule (context_of state) (flat results)
@@ -939,10 +939,10 @@
     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
     |> int ? (fn goal_state =>
       (case test_proof goal_state of
-        Result (SOME _) => goal_state
-      | Result NONE => error (fail_msg (context_of goal_state))
-      | Exn Interrupt => raise Interrupt
-      | Exn exn => raise EXCEPTION (exn, fail_msg (context_of goal_state))))
+        Exn.Result (SOME _) => goal_state
+      | Exn.Result NONE => error (fail_msg (context_of goal_state))
+      | Exn.Exn Interrupt => raise Interrupt
+      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn], fail_msg (context_of goal_state))))
   end;
 
 in
diff -r e0358fac0541 -r c2ee97a963db src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 24 19:44:33 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 24 19:44:35 2007 +0200
@@ -257,7 +257,7 @@
   | exn_msg _ Output.TOPLEVEL_ERROR = "Error."
   | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
   | exn_msg _ (ERROR msg) = msg
-  | exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
+  | exn_msg detailed (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg detailed) exns @ [msg])
   | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   | exn_msg false (THEORY (msg, _)) = msg
   | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)
diff -r e0358fac0541 -r c2ee97a963db src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 24 19:44:33 2007 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 24 19:44:35 2007 +0200
@@ -491,9 +491,9 @@
     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 (capture ast_of) pts;
-    val exns = map_filter get_exn exn_results;
-    val results = map_filter get_result exn_results
+    val exn_results = map (Exn.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 :: _) => raise exn | _ => results) end;
 
 
@@ -522,9 +522,9 @@
           | SOME x => Free (x, T))
         | t => t);
 
-    val exn_results = map (capture (term_of #> free_fixed)) asts;
-    val exns = map_filter get_exn exn_results;
-    val results = map_filter get_result exn_results
+    val exn_results = map (Exn.capture (term_of #> free_fixed)) 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 :: _) => raise exn | _ => results) end;
 
 end;
diff -r e0358fac0541 -r c2ee97a963db src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jul 24 19:44:33 2007 +0200
+++ b/src/Pure/library.ML	Tue Jul 24 19:44:35 2007 +0200
@@ -32,14 +32,6 @@
   val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
   val funpow: int -> ('a -> 'a) -> 'a -> 'a
 
-  (*exceptions*)
-  exception EXCEPTION of exn * string
-  datatype 'a result = Result of 'a | Exn of exn
-  val capture: ('a -> 'b) -> 'a -> 'b result
-  val release: 'a result -> 'a
-  val get_result: 'a result -> 'a option
-  val get_exn: 'a result -> exn option
-
   (*errors*)
   exception SYS_ERROR of string
   val sys_error: string -> 'a
@@ -269,26 +261,6 @@
   | funpow n f x = funpow (n - 1) f (f x);
 
 
-(* exceptions *)
-
-exception EXCEPTION of exn * string;
-
-datatype 'a result =
-  Result of 'a |
-  Exn of exn;
-
-fun capture f x = Result (f x) handle e => Exn e;
-
-fun release (Result y) = y
-  | release (Exn e) = raise e;
-
-fun get_result (Result x) = SOME x
-  | get_result _ = NONE;
-
-fun get_exn (Exn exn) = SOME exn
-  | get_exn _ = NONE;
-
-
 (* errors *)
 
 exception SYS_ERROR of string;
@@ -362,9 +334,9 @@
   let
     val orig_value = ! flag;
     val _ = flag := value;
-    val result = capture f x;
+    val result = Exn.capture f x;
     val _ = flag := orig_value;
-  in release result end;
+  in Exn.release result end;
 
 fun setmp flag value f x = CRITICAL (fn () => setmp_noncritical flag value f x);
 
diff -r e0358fac0541 -r c2ee97a963db src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Jul 24 19:44:33 2007 +0200
+++ b/src/Pure/sign.ML	Tue Jul 24 19:44:35 2007 +0200
@@ -609,13 +609,13 @@
     val termss = fold_rev (multiply o fst) args [[]];
     val typs = map snd args;
 
-    fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
+    fun infer ts = Exn.Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
         (try (Consts.the_constraint consts)) def_type used freeze (ts ~~ typs) |>> map fst)
-      handle TYPE (msg, _, _) => Exn (ERROR msg);
+      handle TYPE (msg, _, _) => Exn.Exn (ERROR msg);
 
     val err_results = map infer termss;
-    val errs = map_filter (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
-    val results = map_filter get_result err_results;
+    val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
+    val results = map_filter Exn.get_result err_results;
 
     val ambiguity = length termss;
     fun ambig_msg () =