more careful treatment of context visibility flag wrt. spurious warnings;
authorwenzelm
Fri Aug 27 19:43:28 2010 +0200 (2010-08-27)
changeset 388314933a3dfd745
parent 38830 51efa72555bb
child 38832 fc0aa40a1b08
more careful treatment of context visibility flag wrt. spurious warnings;
src/Pure/Isar/generic_target.ML
src/Pure/Isar/typedecl.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syntax.ML
src/Pure/context_position.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/Isar/generic_target.ML	Fri Aug 27 18:00:45 2010 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Fri Aug 27 19:43:28 2010 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  fun check_mixfix ctxt (b, extra_tfrees) mx =
     1.5    if null extra_tfrees then mx
     1.6    else
     1.7 -    (warning
     1.8 +    (Context_Position.if_visible ctxt warning
     1.9        ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
    1.10          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
    1.11          (if mx = NoSyn then ""
     2.1 --- a/src/Pure/Isar/typedecl.ML	Fri Aug 27 18:00:45 2010 +0200
     2.2 +++ b/src/Pure/Isar/typedecl.ML	Fri Aug 27 19:43:28 2010 +0200
     2.3 @@ -102,9 +102,10 @@
     2.4      val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
     2.5      val _ =
     2.6        if null ignored then ()
     2.7 -      else warning ("Ignoring sort constraints in type variables(s): " ^
     2.8 -        commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
     2.9 -        "\nin type abbreviation " ^ quote (Binding.str_of b));
    2.10 +      else Context_Position.if_visible ctxt warning
    2.11 +        ("Ignoring sort constraints in type variables(s): " ^
    2.12 +          commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
    2.13 +          "\nin type abbreviation " ^ quote (Binding.str_of b));
    2.14    in rhs end;
    2.15  
    2.16  in
     3.1 --- a/src/Pure/Syntax/parser.ML	Fri Aug 27 18:00:45 2010 +0200
     3.2 +++ b/src/Pure/Syntax/parser.ML	Fri Aug 27 19:43:28 2010 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4    datatype parsetree =
     3.5      Node of string * parsetree list |
     3.6      Tip of Lexicon.token
     3.7 -  val parse: gram -> string -> Lexicon.token list -> parsetree list
     3.8 +  val parse: Proof.context -> gram -> string -> Lexicon.token list -> parsetree list
     3.9    val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
    3.10    val branching_level: int Unsynchronized.ref
    3.11  end;
    3.12 @@ -738,7 +738,7 @@
    3.13    in get_prods (connected_with chains nts nts) [] end;
    3.14  
    3.15  
    3.16 -fun PROCESSS warned prods chains Estate i c states =
    3.17 +fun PROCESSS ctxt warned prods chains Estate i c states =
    3.18    let
    3.19      fun all_prods_for nt = prods_for prods chains true c [nt];
    3.20  
    3.21 @@ -772,7 +772,8 @@
    3.22                  val dummy =
    3.23                    if not (! warned) andalso
    3.24                       length (new_states @ States) > ! branching_level then
    3.25 -                    (warning "Currently parsed expression could be extremely ambiguous.";
    3.26 +                    (Context_Position.if_visible ctxt warning
    3.27 +                      "Currently parsed expression could be extremely ambiguous.";
    3.28                       warned := true)
    3.29                    else ();
    3.30                in
    3.31 @@ -809,7 +810,7 @@
    3.32    in processS [] states ([], []) end;
    3.33  
    3.34  
    3.35 -fun produce warned prods tags chains stateset i indata prev_token =
    3.36 +fun produce ctxt warned prods tags chains stateset i indata prev_token =
    3.37    (case Array.sub (stateset, i) of
    3.38      [] =>
    3.39        let
    3.40 @@ -826,16 +827,16 @@
    3.41        (case indata of
    3.42           [] => Array.sub (stateset, i)
    3.43         | c :: cs =>
    3.44 -         let val (si, sii) = PROCESSS warned prods chains stateset i c s;
    3.45 +         let val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
    3.46           in Array.update (stateset, i, si);
    3.47              Array.update (stateset, i + 1, sii);
    3.48 -            produce warned prods tags chains stateset (i + 1) cs c
    3.49 +            produce ctxt warned prods tags chains stateset (i + 1) cs c
    3.50           end));
    3.51  
    3.52  
    3.53  fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) l;
    3.54  
    3.55 -fun earley prods tags chains startsymbol indata =
    3.56 +fun earley ctxt prods tags chains startsymbol indata =
    3.57    let
    3.58      val start_tag =
    3.59        (case Symtab.lookup tags startsymbol of
    3.60 @@ -846,18 +847,19 @@
    3.61      val Estate = Array.array (s, []);
    3.62      val _ = Array.update (Estate, 0, S0);
    3.63    in
    3.64 -    get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
    3.65 +    get_trees
    3.66 +      (produce ctxt (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
    3.67    end;
    3.68  
    3.69  
    3.70 -fun parse (Gram {tags, prods, chains, ...}) start toks =
    3.71 +fun parse ctxt (Gram {tags, prods, chains, ...}) start toks =
    3.72    let
    3.73      val end_pos =
    3.74        (case try List.last toks of
    3.75          NONE => Position.none
    3.76        | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
    3.77      val r =
    3.78 -      (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
    3.79 +      (case earley ctxt prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
    3.80          [] => raise Fail "Inner syntax: no parse trees"
    3.81        | pts => pts);
    3.82    in r end;
     4.1 --- a/src/Pure/Syntax/syntax.ML	Fri Aug 27 18:00:45 2010 +0200
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Aug 27 19:43:28 2010 +0200
     4.3 @@ -485,7 +485,7 @@
     4.4      val _ = List.app (Lexicon.report_token ctxt) toks;
     4.5  
     4.6      val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
     4.7 -    val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
     4.8 +    val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
     4.9      val len = length pts;
    4.10  
    4.11      val limit = ! ambiguity_limit;
    4.12 @@ -495,7 +495,7 @@
    4.13      if len <= ! ambiguity_level then ()
    4.14      else if ! ambiguity_is_error then error (ambiguity_msg pos)
    4.15      else
    4.16 -      (warning (cat_lines
    4.17 +      (Context_Position.if_visible ctxt warning (cat_lines
    4.18          (("Ambiguous input" ^ Position.str_of pos ^
    4.19            "\nproduces " ^ string_of_int len ^ " parse trees" ^
    4.20            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    4.21 @@ -519,8 +519,8 @@
    4.22  (* read terms *)
    4.23  
    4.24  (*brute-force disambiguation via type-inference*)
    4.25 -fun disambig _ _ [t] = t
    4.26 -  | disambig pp check ts =
    4.27 +fun disambig _ _ _ [t] = t
    4.28 +  | disambig ctxt pp check ts =
    4.29        let
    4.30          val level = ! ambiguity_level;
    4.31          val limit = ! ambiguity_limit;
    4.32 @@ -539,7 +539,8 @@
    4.33          if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
    4.34          else if len = 1 then
    4.35            (if ambiguity > level then
    4.36 -            warning "Fortunately, only one parse tree is type correct.\n\
    4.37 +            Context_Position.if_visible ctxt warning
    4.38 +              "Fortunately, only one parse tree is type correct.\n\
    4.39                \You may still want to disambiguate your grammar or your input."
    4.40            else (); hd results)
    4.41          else cat_error (ambig_msg ()) (cat_lines
    4.42 @@ -551,7 +552,7 @@
    4.43  fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
    4.44    read ctxt is_logtype syn ty (syms, pos)
    4.45    |> map (Type_Ext.decode_term get_sort map_const map_free)
    4.46 -  |> disambig (Printer.pp_show_brackets pp) check;
    4.47 +  |> disambig ctxt (Printer.pp_show_brackets pp) check;
    4.48  
    4.49  
    4.50  (* read types *)
     5.1 --- a/src/Pure/context_position.ML	Fri Aug 27 18:00:45 2010 +0200
     5.2 +++ b/src/Pure/context_position.ML	Fri Aug 27 19:43:28 2010 +0200
     5.3 @@ -9,6 +9,7 @@
     5.4    val is_visible: Proof.context -> bool
     5.5    val set_visible: bool -> Proof.context -> Proof.context
     5.6    val restore_visible: Proof.context -> Proof.context -> Proof.context
     5.7 +  val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
     5.8    val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
     5.9    val report: Proof.context -> Markup.T -> Position.T -> unit
    5.10  end;
    5.11 @@ -26,6 +27,8 @@
    5.12  val set_visible = Data.put;
    5.13  val restore_visible = set_visible o is_visible;
    5.14  
    5.15 +fun if_visible ctxt f x = if is_visible ctxt then f x else ();
    5.16 +
    5.17  fun report_text ctxt markup pos txt =
    5.18    if is_visible ctxt then Position.report_text markup pos txt else ();
    5.19  
     6.1 --- a/src/Pure/variable.ML	Fri Aug 27 18:00:45 2010 +0200
     6.2 +++ b/src/Pure/variable.ML	Fri Aug 27 19:43:28 2010 +0200
     6.3 @@ -506,7 +506,7 @@
     6.4      val tfrees = map #1 extras |> sort_distinct string_ord;
     6.5      val frees = map #2 extras |> sort_distinct string_ord;
     6.6    in
     6.7 -    if null extras then ()
     6.8 +    if null extras orelse not (Context_Position.is_visible ctxt2) then ()
     6.9      else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^
    6.10        space_implode " or " (map quote frees))
    6.11    end;