# HG changeset patch # User haftmann # Date 1256546486 -3600 # Node ID de8cc01e8d9e46b7fed2162e2514d91018a2dfa4 # Parent d6936fd7cda89b046cb7df1edf01730c90d5eed0 legacy warnings for old-style term styles diff -r d6936fd7cda8 -r de8cc01e8d9e src/Pure/Thy/term_style.ML --- a/src/Pure/Thy/term_style.ML Mon Oct 26 09:03:57 2009 +0100 +++ b/src/Pure/Thy/term_style.ML Mon Oct 26 09:41:26 2009 +0100 @@ -54,10 +54,11 @@ >> fold I || Scan.succeed I)); -val parse_bare = Args.context :|-- (fn ctxt => Scan.lift Args.liberal_name +val parse_bare = Args.context :|-- (fn ctxt => (Output.legacy_feature "Old-style antiquotation style."; + Scan.lift Args.liberal_name >> (fn name => fst (Args.context_syntax "style" (Scan.lift (the_style (ProofContext.theory_of ctxt) name)) - (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt)))); + (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt))))); (* predefined styles *) @@ -84,10 +85,13 @@ fun style_parm_premise i = Scan.succeed (fn ctxt => fn t => let val i_str = string_of_int i; + val _ = Output.legacy_feature (quote ("prem" ^ i_str) + ^ " term style encountered; use explicit argument syntax " + ^ quote ("prem " ^ i_str) ^ " instead."); val prems = Logic.strip_imp_prems t; in if i <= length prems then nth prems (i - 1) - else error ("Not enough premises for prem" ^ string_of_int i ^ + else error ("Not enough premises for prem" ^ i_str ^ " in propositon: " ^ Syntax.string_of_term ctxt t) end);