1.1 --- a/src/Pure/Syntax/syntax.ML Sun Jan 27 22:21:34 2008 +0100
1.2 +++ b/src/Pure/Syntax/syntax.ML Sun Jan 27 22:21:35 2008 +0100
1.3 @@ -76,8 +76,9 @@
1.4 Proof.context -> syntax -> bool -> term -> Pretty.T
1.5 val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
1.6 val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
1.7 + val ambiguity_is_error: bool ref
1.8 val ambiguity_level: int ref
1.9 - val ambiguity_is_error: bool ref
1.10 + val ambiguity_limit: int ref
1.11 val parse_sort: Proof.context -> string -> sort
1.12 val parse_typ: Proof.context -> string -> typ
1.13 val parse_term: Proof.context -> string -> term
1.14 @@ -432,8 +433,9 @@
1.15
1.16 (* read_ast *)
1.17
1.18 +val ambiguity_is_error = ref false;
1.19 val ambiguity_level = ref 1;
1.20 -val ambiguity_is_error = ref false;
1.21 +val ambiguity_limit = ref 10;
1.22
1.23 fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root str =
1.24 let
1.25 @@ -441,16 +443,20 @@
1.26 val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
1.27 val chars = Symbol.explode str;
1.28 val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
1.29 + val len = length pts;
1.30
1.31 + val limit = ! ambiguity_limit;
1.32 fun show_pt pt =
1.33 Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
1.34 in
1.35 - if length pts > ! ambiguity_level then
1.36 - if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
1.37 - else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
1.38 - "produces " ^ string_of_int (length pts) ^ " parse trees.");
1.39 - List.app (warning o show_pt) pts)
1.40 - else ();
1.41 + if len <= ! ambiguity_level then ()
1.42 + else if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
1.43 + else
1.44 + (warning (cat_lines
1.45 + (("Ambiguous input " ^ quote str ^ "\n" ^
1.46 + "produces " ^ string_of_int len ^ " parse trees" ^
1.47 + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
1.48 + map show_pt (Library.take (limit, pts)))));
1.49 SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
1.50 end;
1.51
1.52 @@ -473,24 +479,30 @@
1.53 fun disambig _ _ [t] = t
1.54 | disambig pp check ts =
1.55 let
1.56 - val errs = map check ts;
1.57 - val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
1.58 + val level = ! ambiguity_level;
1.59 + val limit = ! ambiguity_limit;
1.60
1.61 val ambiguity = length ts;
1.62 fun ambig_msg () =
1.63 - if ambiguity > 1 andalso ambiguity <= ! ambiguity_level then
1.64 + if ambiguity > 1 andalso ambiguity <= level then
1.65 "Got more than one parse tree.\n\
1.66 - \Retry with smaller ambiguity_level for more information."
1.67 + \Retry with smaller Syntax.ambiguity_level for more information."
1.68 else "";
1.69 +
1.70 + val errs = map check ts;
1.71 + val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
1.72 + val len = length results;
1.73 in
1.74 if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
1.75 - else if length results = 1 then
1.76 - (if ambiguity > ! ambiguity_level then
1.77 + else if len = 1 then
1.78 + (if ambiguity > level then
1.79 warning "Fortunately, only one parse tree is type correct.\n\
1.80 \You may still want to disambiguate your grammar or your input."
1.81 else (); hd results)
1.82 - else cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^
1.83 - cat_lines (map (Pretty.string_of_term pp) ts))
1.84 + else cat_error (ambig_msg ()) (cat_lines
1.85 + (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
1.86 + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
1.87 + map (Pretty.string_of_term pp) (Library.take (limit, results))))
1.88 end;
1.89
1.90 fun standard_parse_term pp check get_sort map_const map_free map_type map_sort