# HG changeset patch
# User wenzelm
# Date 1196178518 -3600
# Node ID 03da46cfab9e7b9f2486326b7c7c38fffe19c672
# Parent  d5a382ccb5cc017a5d04c01c8d6d7745075bbd5f
standard_parse_term: check ambiguous results without changing the result yet;

diff -r d5a382ccb5cc -r 03da46cfab9e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Nov 27 16:48:37 2007 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Nov 27 16:48:38 2007 +0100
@@ -622,8 +622,8 @@
   let
     val thy = theory_of ctxt;
     val (T', _) = TypeInfer.paramify_dummies T 0;
-    fun check t = Exn.Result (Syntax.check_term ctxt (TypeInfer.constrain T' t))
-      handle ERROR msg => Exn.Exn (ERROR msg);
+    fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
+      handle ERROR msg => SOME msg;
     val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
     val read = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort
       map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T';
diff -r d5a382ccb5cc -r 03da46cfab9e src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Nov 27 16:48:37 2007 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Nov 27 16:48:38 2007 +0100
@@ -64,7 +64,7 @@
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
   val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
-  val standard_parse_term: Pretty.pp -> (term -> term Exn.result) ->
+  val standard_parse_term: Pretty.pp -> (term -> string option) ->
     (((string * int) * sort) list -> string * int -> Term.sort) ->
     (string -> string option) -> (string -> string option) ->
     (typ -> typ) -> (sort -> sort) -> Proof.context ->
@@ -473,9 +473,8 @@
 fun disambig _ _ [t] = t
   | disambig pp check ts =
       let
-        val err_results = map check ts;
-        val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
-        val results = map_filter Exn.get_result err_results;
+        val errs = map check ts;
+        val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
 
         val ambiguity = length ts;
         fun ambig_msg () =
@@ -484,7 +483,7 @@
             \Retry with smaller ambiguity_level for more information."
           else "";
       in
-        if null results then cat_error (ambig_msg ()) (cat_lines errs)
+        if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
         else if length results = 1 then
           (if ambiguity > ! ambiguity_level then
             warning "Fortunately, only one parse tree is type correct.\n\
diff -r d5a382ccb5cc -r 03da46cfab9e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Nov 27 16:48:37 2007 +0100
+++ b/src/Pure/sign.ML	Tue Nov 27 16:48:38 2007 +0100
@@ -537,8 +537,7 @@
         (try (Consts.the_constraint consts)) def_type used ~1 (SOME freeze) args |>> map fst
       handle TYPE (msg, _, _) => error msg;
 
-    fun check T t = Exn.Result (singleton (fst o infer) (t, T))
-      handle ERROR msg => Exn.Exn (ERROR msg);
+    fun check T t = (singleton (fst o infer) (t, T); NONE) handle ERROR msg => SOME msg;
     val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
     fun read T = Syntax.standard_parse_term pp (check T) (get_sort thy def_sort) map_const map_free
         (intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;