src/Pure/Syntax/syn_trans.ML

--- a/src/Pure/Syntax/syn_trans.ML	Fri May 21 21:46:25 2004 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Fri May 21 21:47:07 2004 +0200
@@ -50,8 +50,8 @@
   val prop_tr': term -> term
   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-  val pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
-  val ast_to_term: (string -> (term list -> term) option) -> Ast.ast -> term
+  val pts_to_asts: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree list -> Ast.ast list
+  val asts_to_terms: (string -> (term list -> term) option) -> Ast.ast list -> term list
 end;
 
 structure SynTrans: SYN_TRANS =
@@ -452,36 +452,44 @@
 
 
 
-(** pt_to_ast **)
+exception TRANSLATION of string * exn
 
-fun pt_to_ast trf pt =
+(** pts_to_asts **)
+
+fun pts_to_asts trf pts =
   let
     fun trans a args =
       (case trf a of
         None => Ast.mk_appl (Ast.Constant a) args
-      | Some f => f args handle exn
-          => (writeln ("Error in parse ast translation for " ^ quote a);
-              raise exn));
+      | Some f => f args handle exn => raise TRANSLATION (a, exn));
 
     (*translate pt bottom-up*)
     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 exns = mapfilter get_exn exn_results;
+    val results = mapfilter get_result exn_results
   in
-    ast_of pt
+    case results of
+      [] => (case exns of
+        TRANSLATION (a, exn) :: _ =>
+          (writeln ("Error in parse ast translation for " ^ quote a); raise exn)
+      | _ => [])
+    | _ => results
   end;
 
 
 
-(** ast_to_term **)
+(** asts_to_terms **)
 
-fun ast_to_term trf ast =
+fun asts_to_terms trf asts =
   let
     fun trans a args =
       (case trf a of
         None => Term.list_comb (Lexicon.const a, args)
-      | Some f => f args handle exn
-          => (writeln ("Error in parse translation for " ^ quote a);
-              raise exn));
+      | Some f => f args handle exn => raise TRANSLATION (a, exn));
 
     fun term_of (Ast.Constant a) = trans a []
       | term_of (Ast.Variable x) = Lexicon.read_var x
@@ -490,8 +498,18 @@
       | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
           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 exns = mapfilter get_exn exn_results;
+    val results = mapfilter get_result exn_results
   in
-    term_of ast
+    case results of
+      [] => (case exns of
+        TRANSLATION (a, exn) :: _ =>
+          (writeln ("Error in parse translation for " ^ quote a); raise exn)
+      | _ => [])
+    | _ => results
   end;
 
 end;