src/Pure/Syntax/syntax.ML
changeset 25476 03da46cfab9e
parent 25394 db25c98f32e1
child 25993 d542486e39e7
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 27 16:48:37 2007 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 27 16:48:38 2007 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4    val print_trans: syntax -> unit
     1.5    val print_syntax: syntax -> unit
     1.6    val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
     1.7 -  val standard_parse_term: Pretty.pp -> (term -> term Exn.result) ->
     1.8 +  val standard_parse_term: Pretty.pp -> (term -> string option) ->
     1.9      (((string * int) * sort) list -> string * int -> Term.sort) ->
    1.10      (string -> string option) -> (string -> string option) ->
    1.11      (typ -> typ) -> (sort -> sort) -> Proof.context ->
    1.12 @@ -473,9 +473,8 @@
    1.13  fun disambig _ _ [t] = t
    1.14    | disambig pp check ts =
    1.15        let
    1.16 -        val err_results = map check ts;
    1.17 -        val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
    1.18 -        val results = map_filter Exn.get_result err_results;
    1.19 +        val errs = map check ts;
    1.20 +        val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
    1.21  
    1.22          val ambiguity = length ts;
    1.23          fun ambig_msg () =
    1.24 @@ -484,7 +483,7 @@
    1.25              \Retry with smaller ambiguity_level for more information."
    1.26            else "";
    1.27        in
    1.28 -        if null results then cat_error (ambig_msg ()) (cat_lines errs)
    1.29 +        if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
    1.30          else if length results = 1 then
    1.31            (if ambiguity > ! ambiguity_level then
    1.32              warning "Fortunately, only one parse tree is type correct.\n\