# HG changeset patch # User wenzelm # Date 1282931008 -7200 # Node ID 4933a3dfd7454396997a149e77da700f2e3a5abb # Parent 51efa72555bbf4f741240a5fa3ef04edd25d4e9d more careful treatment of context visibility flag wrt. spurious warnings; diff -r 51efa72555bb -r 4933a3dfd745 src/Pure/Isar/generic_target.ML --- 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 "" diff -r 51efa72555bb -r 4933a3dfd745 src/Pure/Isar/typedecl.ML --- 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 diff -r 51efa72555bb -r 4933a3dfd745 src/Pure/Syntax/parser.ML --- 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; diff -r 51efa72555bb -r 4933a3dfd745 src/Pure/Syntax/syntax.ML --- 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 *) diff -r 51efa72555bb -r 4933a3dfd745 src/Pure/context_position.ML --- 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 (); diff -r 51efa72555bb -r 4933a3dfd745 src/Pure/variable.ML --- 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;