more careful treatment of context visibility flag wrt. spurious warnings;

--- a/src/Pure/Isar/generic_target.ML	Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Aug 27 19:43:28 2010 +0200
@@ -41,7 +41,7 @@
 fun check_mixfix ctxt (b, extra_tfrees) mx =
   if null extra_tfrees then mx
   else
-    (warning
+    (Context_Position.if_visible ctxt warning
       ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
         commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
         (if mx = NoSyn then ""

--- a/src/Pure/Isar/typedecl.ML	Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Fri Aug 27 19:43:28 2010 +0200
@@ -102,9 +102,10 @@
     val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
     val _ =
       if null ignored then ()
-      else warning ("Ignoring sort constraints in type variables(s): " ^
-        commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
-        "\nin type abbreviation " ^ quote (Binding.str_of b));
+      else Context_Position.if_visible ctxt warning
+        ("Ignoring sort constraints in type variables(s): " ^
+          commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
+          "\nin type abbreviation " ^ quote (Binding.str_of b));
   in rhs end;
 
 in

--- a/src/Pure/Syntax/parser.ML	Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Aug 27 19:43:28 2010 +0200
@@ -15,7 +15,7 @@
   datatype parsetree =
     Node of string * parsetree list |
     Tip of Lexicon.token
-  val parse: gram -> string -> Lexicon.token list -> parsetree list
+  val parse: Proof.context -> gram -> string -> Lexicon.token list -> parsetree list
   val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
   val branching_level: int Unsynchronized.ref
 end;
@@ -738,7 +738,7 @@
   in get_prods (connected_with chains nts nts) [] end;
 
 
-fun PROCESSS warned prods chains Estate i c states =
+fun PROCESSS ctxt warned prods chains Estate i c states =
   let
     fun all_prods_for nt = prods_for prods chains true c [nt];
 
@@ -772,7 +772,8 @@
                 val dummy =
                   if not (! warned) andalso
                      length (new_states @ States) > ! branching_level then
-                    (warning "Currently parsed expression could be extremely ambiguous.";
+                    (Context_Position.if_visible ctxt warning
+                      "Currently parsed expression could be extremely ambiguous.";
                      warned := true)
                   else ();
               in
@@ -809,7 +810,7 @@
   in processS [] states ([], []) end;
 
 
-fun produce warned prods tags chains stateset i indata prev_token =
+fun produce ctxt warned prods tags chains stateset i indata prev_token =
   (case Array.sub (stateset, i) of
     [] =>
       let
@@ -826,16 +827,16 @@
       (case indata of
          [] => Array.sub (stateset, i)
        | c :: cs =>
-         let val (si, sii) = PROCESSS warned prods chains stateset i c s;
+         let val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
          in Array.update (stateset, i, si);
             Array.update (stateset, i + 1, sii);
-            produce warned prods tags chains stateset (i + 1) cs c
+            produce ctxt warned prods tags chains stateset (i + 1) cs c
          end));
 
 
 fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) l;
 
-fun earley prods tags chains startsymbol indata =
+fun earley ctxt prods tags chains startsymbol indata =
   let
     val start_tag =
       (case Symtab.lookup tags startsymbol of
@@ -846,18 +847,19 @@
     val Estate = Array.array (s, []);
     val _ = Array.update (Estate, 0, S0);
   in
-    get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
+    get_trees
+      (produce ctxt (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
   end;
 
 
-fun parse (Gram {tags, prods, chains, ...}) start toks =
+fun parse ctxt (Gram {tags, prods, chains, ...}) start toks =
   let
     val end_pos =
       (case try List.last toks of
         NONE => Position.none
       | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
     val r =
-      (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
+      (case earley ctxt prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
         [] => raise Fail "Inner syntax: no parse trees"
       | pts => pts);
   in r end;

--- a/src/Pure/Syntax/syntax.ML	Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Aug 27 19:43:28 2010 +0200
@@ -485,7 +485,7 @@
     val _ = List.app (Lexicon.report_token ctxt) toks;
 
     val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
-    val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
+    val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
     val len = length pts;
 
     val limit = ! ambiguity_limit;
@@ -495,7 +495,7 @@
     if len <= ! ambiguity_level then ()
     else if ! ambiguity_is_error then error (ambiguity_msg pos)
     else
-      (warning (cat_lines
+      (Context_Position.if_visible ctxt warning (cat_lines
         (("Ambiguous input" ^ Position.str_of pos ^
           "\nproduces " ^ string_of_int len ^ " parse trees" ^
           (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
@@ -519,8 +519,8 @@
 (* read terms *)
 
 (*brute-force disambiguation via type-inference*)
-fun disambig _ _ [t] = t
-  | disambig pp check ts =
+fun disambig _ _ _ [t] = t
+  | disambig ctxt pp check ts =
       let
         val level = ! ambiguity_level;
         val limit = ! ambiguity_limit;
@@ -539,7 +539,8 @@
         if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
         else if len = 1 then
           (if ambiguity > level then
-            warning "Fortunately, only one parse tree is type correct.\n\
+            Context_Position.if_visible ctxt warning
+              "Fortunately, only one parse tree is type correct.\n\
               \You may still want to disambiguate your grammar or your input."
           else (); hd results)
         else cat_error (ambig_msg ()) (cat_lines
@@ -551,7 +552,7 @@
 fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
   read ctxt is_logtype syn ty (syms, pos)
   |> map (Type_Ext.decode_term get_sort map_const map_free)
-  |> disambig (Printer.pp_show_brackets pp) check;
+  |> disambig ctxt (Printer.pp_show_brackets pp) check;
 
 
 (* read types *)

--- a/src/Pure/context_position.ML	Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/context_position.ML	Fri Aug 27 19:43:28 2010 +0200
@@ -9,6 +9,7 @@
   val is_visible: Proof.context -> bool
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
+  val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
   val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
   val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
@@ -26,6 +27,8 @@
 val set_visible = Data.put;
 val restore_visible = set_visible o is_visible;
 
+fun if_visible ctxt f x = if is_visible ctxt then f x else ();
+
 fun report_text ctxt markup pos txt =
   if is_visible ctxt then Position.report_text markup pos txt else ();
 

--- a/src/Pure/variable.ML	Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/variable.ML	Fri Aug 27 19:43:28 2010 +0200
@@ -506,7 +506,7 @@
     val tfrees = map #1 extras |> sort_distinct string_ord;
     val frees = map #2 extras |> sort_distinct string_ord;
   in
-    if null extras then ()
+    if null extras orelse not (Context_Position.is_visible ctxt2) then ()
     else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^
       space_implode " or " (map quote frees))
   end;