Modified functions pt_to_ast and ast_to_term to improve handling
of errors in parse (ast) translations caused by ambiguous input.

--- 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;

--- a/src/Pure/Syntax/syntax.ML	Fri May 21 21:46:25 2004 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri May 21 21:47:07 2004 +0200
@@ -339,9 +339,9 @@
 
     fun show_pt pt =
       let
-        val raw_ast = SynTrans.pt_to_ast (K None) pt;
+        val [raw_ast] = SynTrans.pts_to_asts (K None) [pt];
         val _ = writeln ("raw: " ^ Ast.str_of_ast raw_ast);
-        val pre_ast = SynTrans.pt_to_ast (lookup_tr parse_ast_trtab) pt;
+        val [pre_ast] = SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) [pt];
         val _ = Ast.normalize true true (lookup_ruletab parse_ruletab) pre_ast;
       in () end;
   in seq show_pt (Parser.parse gram root toks) end;
@@ -359,7 +359,7 @@
     val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
 
     fun show_pt pt =
-      warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
+      warning (Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts (K None) [pt]))));
   in
     if length pts > ! ambiguity_level then
         if ! ambiguity_is_error then
@@ -369,7 +369,7 @@
              warning "produces the following parse trees:";
              seq show_pt pts)
     else ();
-    map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts
+    SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) pts
   end;
 
 
@@ -380,7 +380,7 @@
     val {parse_ruletab, parse_trtab, ...} = tabs;
     val asts = read_asts syn false (SynExt.typ_to_nonterm ty) str;
   in
-    map (SynTrans.ast_to_term (lookup_tr parse_trtab))
+    SynTrans.asts_to_terms (lookup_tr parse_trtab)
       (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts)
   end;