# HG changeset patch
# User bulwahn
# Date 1311583251 -7200
# Node ID efc6f0a81c364427dd134ad2771551ba1196b681
# Parent  521de6ab277a29751ba2fe15740c70cd3e49bff3
added legacy warning to old code generation commands

diff -r 521de6ab277a -r efc6f0a81c36 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Jul 23 23:33:59 2011 +0200
+++ b/src/Pure/codegen.ML	Mon Jul 25 10:40:51 2011 +0200
@@ -1012,6 +1012,7 @@
    || Scan.repeat1 (Parse.term >> pair "")) >>
   (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
     let
+      val _ = legacy_feature "Old code generation command -- use export_code instead";
       val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
       val (code, gr) = generate_code thy mode' modules module xs;
       val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>