tuned exeption handling (capture/release);

--- a/src/Pure/Syntax/syn_trans.ML	Sat Jun 05 13:05:37 2004 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Sat Jun 05 13:06:04 2004 +0200
@@ -452,9 +452,9 @@
 
 
 
-exception TRANSLATION of string * exn
+(** pts_to_asts **)
 
-(** pts_to_asts **)
+exception TRANSLATION of string * exn;
 
 fun pts_to_asts trf pts =
   let
@@ -467,17 +467,14 @@
     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 (fn pt => Result (ast_of pt) handle exn => Exn exn) pts;
+    val exn_results = map (capture ast_of) pts;
     val exns = mapfilter get_exn exn_results;
     val results = mapfilter get_result exn_results
   in
-    case results of
-      [] => (case exns of
-        TRANSLATION (a, exn) :: _ =>
-          (writeln ("Error in parse ast translation for " ^ quote a); raise exn)
-      | _ => [])
-    | _ => results
+    (case (results, exns) of
+      ([], TRANSLATION (a, exn) :: _) =>
+        (writeln ("Error in parse ast translation for " ^ quote a); raise exn)
+    | _ => results)
   end;
 
 
@@ -499,17 +496,14 @@
           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 (fn t => Result (term_of t) handle exn => Exn exn) asts;
+    val exn_results = map (capture term_of) asts;
     val exns = mapfilter get_exn exn_results;
     val results = mapfilter get_result exn_results
   in
-    case results of
-      [] => (case exns of
-        TRANSLATION (a, exn) :: _ =>
-          (writeln ("Error in parse translation for " ^ quote a); raise exn)
-      | _ => [])
-    | _ => results
+    (case (results, exns) of
+      ([], TRANSLATION (a, exn) :: _) =>
+        (writeln ("Error in parse translation for " ^ quote a); raise exn)
+    | _ => results)
   end;
 
 end;

--- a/src/Pure/library.ML	Sat Jun 05 13:05:37 2004 +0200
+++ b/src/Pure/library.ML	Sat Jun 05 13:06:04 2004 +0200
@@ -47,6 +47,11 @@
   exception ERROR
   val try: ('a -> 'b) -> 'a -> 'b option
   val can: ('a -> 'b) -> 'a -> bool
+  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
 
   (*pairs*)
   val pair: 'a -> 'b -> 'a * 'b
@@ -338,6 +343,22 @@
 fun can f x = is_some (try f x);
 
 
+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;
+
+
 
 (** pairs **)