added legacy warning to old code generation commands
authorbulwahn
Mon, 25 Jul 2011 10:40:51 +0200
changeset 43955 efc6f0a81c36
parent 43954 521de6ab277a
child 43956 4611af362cd0
added legacy warning to old code generation commands
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 () =>