legacy warnings for old-style term styles
authorhaftmann
Mon Oct 26 09:41:26 2009 +0100 (2009-10-26)
changeset 33184de8cc01e8d9e
parent 33176 d6936fd7cda8
child 33185 247f6c6969d9
legacy warnings for old-style term styles
src/Pure/Thy/term_style.ML
     1.1 --- a/src/Pure/Thy/term_style.ML	Mon Oct 26 09:03:57 2009 +0100
     1.2 +++ b/src/Pure/Thy/term_style.ML	Mon Oct 26 09:41:26 2009 +0100
     1.3 @@ -54,10 +54,11 @@
     1.4        >> fold I
     1.5    || Scan.succeed I));
     1.6  
     1.7 -val parse_bare = Args.context :|-- (fn ctxt => Scan.lift Args.liberal_name
     1.8 +val parse_bare = Args.context :|-- (fn ctxt => (Output.legacy_feature "Old-style antiquotation style.";
     1.9 +  Scan.lift Args.liberal_name
    1.10    >> (fn name => fst (Args.context_syntax "style"
    1.11         (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
    1.12 -          (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt))));
    1.13 +          (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt)))));
    1.14  
    1.15  
    1.16  (* predefined styles *)
    1.17 @@ -84,10 +85,13 @@
    1.18  fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
    1.19    let
    1.20      val i_str = string_of_int i;
    1.21 +    val _ = Output.legacy_feature (quote ("prem" ^ i_str)
    1.22 +      ^ " term style encountered; use explicit argument syntax "
    1.23 +      ^ quote ("prem " ^ i_str) ^ " instead.");
    1.24      val prems = Logic.strip_imp_prems t;
    1.25    in
    1.26      if i <= length prems then nth prems (i - 1)
    1.27 -    else error ("Not enough premises for prem" ^ string_of_int i ^
    1.28 +    else error ("Not enough premises for prem" ^ i_str ^
    1.29        " in propositon: " ^ Syntax.string_of_term ctxt t)
    1.30    end);
    1.31