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