1.1 --- a/src/Pure/Syntax/syn_trans.ML	Sat Jun 05 13:05:37 2004 +0200
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Sat Jun 05 13:06:04 2004 +0200
     1.3 @@ -452,9 +452,9 @@
     1.4  
     1.5  
     1.6  
     1.7 -exception TRANSLATION of string * exn
     1.8 +(** pts_to_asts **)
     1.9  
    1.10 -(** pts_to_asts **)
    1.11 +exception TRANSLATION of string * exn;
    1.12  
    1.13  fun pts_to_asts trf pts =
    1.14    let
    1.15 @@ -467,17 +467,14 @@
    1.16      fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
    1.17        | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
    1.18  
    1.19 -    val exn_results =
    1.20 -      map (fn pt => Result (ast_of pt) handle exn => Exn exn) pts;
    1.21 +    val exn_results = map (capture ast_of) pts;
    1.22      val exns = mapfilter get_exn exn_results;
    1.23      val results = mapfilter get_result exn_results
    1.24    in
    1.25 -    case results of
    1.26 -      [] => (case exns of
    1.27 -        TRANSLATION (a, exn) :: _ =>
    1.28 -          (writeln ("Error in parse ast translation for " ^ quote a); raise exn)
    1.29 -      | _ => [])
    1.30 -    | _ => results
    1.31 +    (case (results, exns) of
    1.32 +      ([], TRANSLATION (a, exn) :: _) =>
    1.33 +        (writeln ("Error in parse ast translation for " ^ quote a); raise exn)
    1.34 +    | _ => results)
    1.35    end;
    1.36  
    1.37  
    1.38 @@ -499,17 +496,14 @@
    1.39            Term.list_comb (term_of ast, map term_of asts)
    1.40        | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
    1.41  
    1.42 -    val exn_results =
    1.43 -      map (fn t => Result (term_of t) handle exn => Exn exn) asts;
    1.44 +    val exn_results = map (capture term_of) asts;
    1.45      val exns = mapfilter get_exn exn_results;
    1.46      val results = mapfilter get_result exn_results
    1.47    in
    1.48 -    case results of
    1.49 -      [] => (case exns of
    1.50 -        TRANSLATION (a, exn) :: _ =>
    1.51 -          (writeln ("Error in parse translation for " ^ quote a); raise exn)
    1.52 -      | _ => [])
    1.53 -    | _ => results
    1.54 +    (case (results, exns) of
    1.55 +      ([], TRANSLATION (a, exn) :: _) =>
    1.56 +        (writeln ("Error in parse translation for " ^ quote a); raise exn)
    1.57 +    | _ => results)
    1.58    end;
    1.59  
    1.60  end;

     2.1 --- a/src/Pure/library.ML	Sat Jun 05 13:05:37 2004 +0200
     2.2 +++ b/src/Pure/library.ML	Sat Jun 05 13:06:04 2004 +0200
     2.3 @@ -47,6 +47,11 @@
     2.4    exception ERROR
     2.5    val try: ('a -> 'b) -> 'a -> 'b option
     2.6    val can: ('a -> 'b) -> 'a -> bool
     2.7 +  datatype 'a result = Result of 'a | Exn of exn
     2.8 +  val capture: ('a -> 'b) -> 'a -> 'b result
     2.9 +  val release: 'a result -> 'a
    2.10 +  val get_result: 'a result -> 'a option
    2.11 +  val get_exn: 'a result -> exn option
    2.12  
    2.13    (*pairs*)
    2.14    val pair: 'a -> 'b -> 'a * 'b
    2.15 @@ -338,6 +343,22 @@
    2.16  fun can f x = is_some (try f x);
    2.17  
    2.18  
    2.19 +datatype 'a result =
    2.20 +  Result of 'a |
    2.21 +  Exn of exn;
    2.22 +
    2.23 +fun capture f x = Result (f x) handle e => Exn e;
    2.24 +
    2.25 +fun release (Result y) = y
    2.26 +  | release (Exn e) = raise e;
    2.27 +
    2.28 +fun get_result (Result x) = Some x
    2.29 +  | get_result _ = None;
    2.30 +
    2.31 +fun get_exn (Exn exn) = Some exn
    2.32 +  | get_exn _ = None;
    2.33 +
    2.34 +
    2.35  
    2.36  (** pairs **)
    2.37