# HG changeset patch
# User clasohm
# Date 791206236 -3600
# Node ID b118d1ea0dfd995fcf09843ffc8af1fc53c3ab39
# Parent  d7dcba167ed804f69317c84337310bf0b6d5de9a
moved ambiguity_level from sign.ML to Syntax/syntax.ML

diff -r d7dcba167ed8 -r b118d1ea0dfd src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jan 27 12:28:05 1995 +0100
+++ b/src/Pure/Syntax/syntax.ML	Fri Jan 27 12:30:36 1995 +0100
@@ -60,6 +60,7 @@
   val string_of_typ: syntax -> typ -> string
   val simple_string_of_typ: typ -> string
   val simple_pprint_typ: typ -> pprint_args -> unit
+  val ambiguity_level: int ref
 end;
 
 functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
@@ -302,6 +303,8 @@
 
 (* read_ast *)
 
+val ambiguity_level = ref 1;
+
 fun read_asts (Syntax tabs) xids root str =
   let
     val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
@@ -310,9 +313,10 @@
 
     fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
   in
-    if length pts > 1 then
+    if length pts > !ambiguity_level then
       (writeln ("Warning: Ambiguous input " ^ quote str);
-       writeln "produces the following parse trees:"; seq show_pt pts)
+       writeln "produces the following parse trees:";
+       seq show_pt pts)
     else ();
     map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts
   end;