explicit treatment of legacy_features;
authorwenzelm
Mon Apr 30 13:32:58 2007 +0200 (2007-04-30)
changeset 228260f4c501a691e
parent 22825 bd774e01d6d5
child 22827 7dc27b37f7f7
explicit treatment of legacy_features;
NEWS
src/Provers/induct_method.ML
src/Pure/General/output.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Syntax/mixfix.ML
src/Pure/old_goals.ML
     1.1 --- a/NEWS	Mon Apr 30 13:22:35 2007 +0200
     1.2 +++ b/NEWS	Mon Apr 30 13:32:58 2007 +0200
     1.3 @@ -6,6 +6,10 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* More uniform information about legacy features, notably a
     1.8 +warning/error of "Legacy feature: ...", depending on the state of the
     1.9 +tolerate_legacy_features flag (default true).
    1.10 +
    1.11  * Theory syntax: the header format ``theory A = B + C:'' has been
    1.12  discontinued in favour of ``theory A imports B C begin''.  Use isatool
    1.13  fixheaders to convert existing theory files.  INCOMPATIBILITY.
     2.1 --- a/src/Provers/induct_method.ML	Mon Apr 30 13:22:35 2007 +0200
     2.2 +++ b/src/Provers/induct_method.ML	Mon Apr 30 13:32:58 2007 +0200
     2.3 @@ -95,7 +95,7 @@
     2.4  fun make_cases is_open rule =
     2.5    RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
     2.6  
     2.7 -fun warn_open true = warning "Encountered open rule cases -- deprecated"
     2.8 +fun warn_open true = legacy_feature "open rule cases in proof method"
     2.9    | warn_open false = ();
    2.10  
    2.11  
     3.1 --- a/src/Pure/General/output.ML	Mon Apr 30 13:22:35 2007 +0200
     3.2 +++ b/src/Pure/General/output.ML	Mon Apr 30 13:32:58 2007 +0200
     3.3 @@ -11,6 +11,8 @@
     3.4    val priority: string -> unit
     3.5    val tracing: string -> unit
     3.6    val warning: string -> unit
     3.7 +  val tolerate_legacy_features: bool ref
     3.8 +  val legacy_feature: string -> unit
     3.9    val timing: bool ref
    3.10    val cond_timeit: bool -> (unit -> 'a) -> 'a
    3.11    val timeit: (unit -> 'a) -> 'a
    3.12 @@ -110,6 +112,10 @@
    3.13  fun tracing s = ! tracing_fn (output s);
    3.14  fun warning s = ! warning_fn (output s);
    3.15  
    3.16 +val tolerate_legacy_features = ref true;
    3.17 +fun legacy_feature s =
    3.18 +  (if ! tolerate_legacy_features then warning else error) ("Legacy feature: " ^ s);
    3.19 +
    3.20  fun no_warnings f = setmp warning_fn (K ()) f;
    3.21  
    3.22  val debugging = ref false;
     4.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 30 13:22:35 2007 +0200
     4.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 30 13:32:58 2007 +0200
     4.3 @@ -268,7 +268,7 @@
     4.4      if is_none (ThyLoad.check_file NONE path) then ()
     4.5      else
     4.6        let
     4.7 -        val _ = warning ("Loading legacy ML script " ^ quote (Path.implode path));
     4.8 +        val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path));
     4.9          val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
    4.10          val tr_name = if time then "time_use" else "use";
    4.11        in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
     5.1 --- a/src/Pure/Syntax/mixfix.ML	Mon Apr 30 13:22:35 2007 +0200
     5.2 +++ b/src/Pure/Syntax/mixfix.ML	Mon Apr 30 13:32:58 2007 +0200
     5.3 @@ -105,7 +105,7 @@
     5.4  
     5.5  val strip_esc = implode o strip o Symbol.explode;
     5.6  
     5.7 -fun deprecated c = (warning ("Unnamed infix operator " ^ quote c ^ " -- deprecated"); c);
     5.8 +fun deprecated c = (legacy_feature ("unnamed infix operator " ^ quote c); c);
     5.9  
    5.10  fun type_name t (InfixName _) = t
    5.11    | type_name t (InfixlName _) = t
     6.1 --- a/src/Pure/old_goals.ML	Mon Apr 30 13:22:35 2007 +0200
     6.2 +++ b/src/Pure/old_goals.ML	Mon Apr 30 13:32:58 2007 +0200
     6.3 @@ -152,7 +152,7 @@
     6.4  *)
     6.5  fun prepare_proof atomic rths chorn =
     6.6    let
     6.7 -      val _ = warning "Obsolete goal command encountered";
     6.8 +      val _ = legacy_feature "old goal command";
     6.9        val {thy, t=horn,...} = rep_cterm chorn;
    6.10        val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
    6.11        val (As, B) = Logic.strip_horn horn;
    6.12 @@ -373,7 +373,7 @@
    6.13  (*simple version with minimal amount of checking and postprocessing*)
    6.14  fun simple_prove_goal_cterm G f =
    6.15    let
    6.16 -    val _ = warning "Obsolete goal command encountered";
    6.17 +    val _ = legacy_feature "old goal command";
    6.18      val As = Drule.strip_imp_prems G;
    6.19      val B = Drule.strip_imp_concl G;
    6.20      val asms = map Assumption.assume As;