standard_parse_term: check ambiguous results without changing the result yet;
authorwenzelm
Tue Nov 27 16:48:38 2007 +0100 (2007-11-27 ago)
changeset 2547603da46cfab9e
parent 25475 d5a382ccb5cc
child 25477 d350aa8cc53d
standard_parse_term: check ambiguous results without changing the result yet;
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Nov 27 16:48:37 2007 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Nov 27 16:48:38 2007 +0100
     1.3 @@ -622,8 +622,8 @@
     1.4    let
     1.5      val thy = theory_of ctxt;
     1.6      val (T', _) = TypeInfer.paramify_dummies T 0;
     1.7 -    fun check t = Exn.Result (Syntax.check_term ctxt (TypeInfer.constrain T' t))
     1.8 -      handle ERROR msg => Exn.Exn (ERROR msg);
     1.9 +    fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
    1.10 +      handle ERROR msg => SOME msg;
    1.11      val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
    1.12      val read = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort
    1.13        map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T';
     2.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 27 16:48:37 2007 +0100
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 27 16:48:38 2007 +0100
     2.3 @@ -64,7 +64,7 @@
     2.4    val print_trans: syntax -> unit
     2.5    val print_syntax: syntax -> unit
     2.6    val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
     2.7 -  val standard_parse_term: Pretty.pp -> (term -> term Exn.result) ->
     2.8 +  val standard_parse_term: Pretty.pp -> (term -> string option) ->
     2.9      (((string * int) * sort) list -> string * int -> Term.sort) ->
    2.10      (string -> string option) -> (string -> string option) ->
    2.11      (typ -> typ) -> (sort -> sort) -> Proof.context ->
    2.12 @@ -473,9 +473,8 @@
    2.13  fun disambig _ _ [t] = t
    2.14    | disambig pp check ts =
    2.15        let
    2.16 -        val err_results = map check ts;
    2.17 -        val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
    2.18 -        val results = map_filter Exn.get_result err_results;
    2.19 +        val errs = map check ts;
    2.20 +        val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
    2.21  
    2.22          val ambiguity = length ts;
    2.23          fun ambig_msg () =
    2.24 @@ -484,7 +483,7 @@
    2.25              \Retry with smaller ambiguity_level for more information."
    2.26            else "";
    2.27        in
    2.28 -        if null results then cat_error (ambig_msg ()) (cat_lines errs)
    2.29 +        if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
    2.30          else if length results = 1 then
    2.31            (if ambiguity > ! ambiguity_level then
    2.32              warning "Fortunately, only one parse tree is type correct.\n\
     3.1 --- a/src/Pure/sign.ML	Tue Nov 27 16:48:37 2007 +0100
     3.2 +++ b/src/Pure/sign.ML	Tue Nov 27 16:48:38 2007 +0100
     3.3 @@ -537,8 +537,7 @@
     3.4          (try (Consts.the_constraint consts)) def_type used ~1 (SOME freeze) args |>> map fst
     3.5        handle TYPE (msg, _, _) => error msg;
     3.6  
     3.7 -    fun check T t = Exn.Result (singleton (fst o infer) (t, T))
     3.8 -      handle ERROR msg => Exn.Exn (ERROR msg);
     3.9 +    fun check T t = (singleton (fst o infer) (t, T); NONE) handle ERROR msg => SOME msg;
    3.10      val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
    3.11      fun read T = Syntax.standard_parse_term pp (check T) (get_sort thy def_sort) map_const map_free
    3.12          (intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;