dropped legacy finally

--- a/src/Doc/Codegen/Further.thy	Sun Feb 09 19:10:12 2014 +0000
+++ b/src/Doc/Codegen/Further.thy	Sun Feb 09 21:37:27 2014 +0100
@@ -33,7 +33,7 @@
   rather than function definitions are always curried.
 
   The second aspect affects user-defined adaptations with @{command
-  code_const}.  For regular terms, the @{text Scala} serializer prints
+  code_printing}.  For regular terms, the @{text Scala} serializer prints
   all type arguments explicitly.  For user-defined term adaptations
   this is only possible for adaptations which take no arguments: here
   the type arguments are just appended.  Otherwise they are ignored;

--- a/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 09 19:10:12 2014 +0000
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 09 21:37:27 2014 +0100
@@ -2386,13 +2386,7 @@
     @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_printing"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_identifier"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
@@ -2494,34 +2488,12 @@
       | printing_module ) + '|' )
     ;
 
-    @@{command (HOL) code_const} (const + @'and') \<newline>
-      ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
-    ;
-
-    @@{command (HOL) code_type} (typeconstructor + @'and') \<newline>
-      ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
-    ;
-
-    @@{command (HOL) code_class} (class + @'and') \<newline>
-      ( ( '(' target \<newline> ( @{syntax string} ? + @'and' ) ')' ) + )
-    ;
-
-    @@{command (HOL) code_instance} (( typeconstructor '::' class ) + @'and') \<newline>
-      ( ( '(' target ( '-' ? + @'and' ) ')' ) + )
-    ;
-
-    @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
-    ;
-
     @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
       | symbol_class | symbol_class_relation | symbol_class_instance
       | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \<newline>
       ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
     ;
 
-    @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
-    ;
-
     @@{command (HOL) code_monad} const const target
     ;
 
@@ -2629,10 +2601,7 @@
   \item @{command (HOL) "code_printing"} associates a series of symbols
   (constants, type constructors, classes, class relations, instances,
   module names) with target-specific serializations; omitting a serialization
-  deletes an existing serialization.  Legacy variants of this are
-  @{command (HOL) "code_const"}, @{command (HOL) "code_type"},
-  @{command (HOL) "code_class"}, @{command (HOL) "code_instance"},
-  @{command (HOL) "code_include"}.
+  deletes an existing serialization.
 
   \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
   to generate monadic code for Haskell.
@@ -2642,8 +2611,6 @@
   module names) with target-specific hints how these symbols shall be named.
   These hints gain precedence over names for symbols with no hints at all.
   Conflicting hints are subject to name disambiguation.
-  @{command (HOL) "code_modulename"} is a legacy variant for
-  @{command (HOL) "code_identifier"} on module names.
   \emph{Warning:} It is at the discretion
   of the user to ensure that name prefixes of identifiers in compound
   statements like type classes or datatypes are still the same.

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Feb 09 19:10:12 2014 +0000
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Feb 09 21:37:27 2014 +0100
@@ -575,7 +575,7 @@
 
 text {* Adaption layer *}
 
-code_include Haskell "Heap"
+code_printing code_module "Heap" \<rightharpoonup> (Haskell)
 {*import qualified Control.Monad;
 import qualified Control.Monad.ST;
 import qualified Data.STRef;
@@ -620,7 +620,7 @@
 
 subsubsection {* Scala *}
 
-code_include Scala "Heap"
+code_printing code_module "Heap" \<rightharpoonup> (Scala)
 {*object Heap {
   def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
 }

--- a/src/Tools/Code/code_target.ML	Sun Feb 09 19:10:12 2014 +0000
+++ b/src/Tools/Code/code_target.ML	Sun Feb 09 21:37:27 2014 +0100
@@ -53,16 +53,9 @@
   type identifier_data
   val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
     -> theory -> theory
-  type raw_const_syntax = Code_Printer.raw_const_syntax
-  type tyco_syntax = Code_Printer.tyco_syntax
-  val set_printings: (raw_const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
+  val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
     -> theory -> theory
-  val add_const_syntax: string -> string -> raw_const_syntax option -> theory -> theory
-  val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
-  val add_class_syntax: string -> class -> string option -> theory -> theory
-  val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
-  val add_include: string -> string * (string * string list) option -> theory -> theory
 
   val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
 
@@ -584,15 +577,6 @@
 val set_identifiers = gen_set_identifiers cert_name_decls;
 val set_identifiers_cmd = gen_set_identifiers read_name_decls;
 
-fun add_module_alias_cmd target aliasses thy =
-  let
-    val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\"";
-  in
-    fold (fn (sym, name) => set_identifier
-      (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name))))
-      aliasses thy
-  end;
-
 
 (* custom printings *)
 
@@ -620,62 +604,9 @@
 val set_printings = gen_set_printings cert_printings;
 val set_printings_cmd = gen_set_printings read_printings;
 
-fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy =
-  let
-    val _ = legacy_feature "prefer \"code_printing\" for custom serialisations"
-    val x = prep_x thy raw_x;
-  in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end;
-
-fun gen_add_const_syntax prep_const =
-  gen_add_syntax Constant prep_const check_const_syntax;
-
-fun gen_add_tyco_syntax prep_tyco =
-  gen_add_syntax Type_Constructor prep_tyco check_tyco_syntax;
-
-fun gen_add_class_syntax prep_class =
-  gen_add_syntax Type_Class prep_class ((K o K o K) I);
-
-fun gen_add_instance_syntax prep_inst =
-  gen_add_syntax Class_Instance prep_inst ((K o K o K) I);
-
-fun gen_add_include prep_const target (name, some_content) thy =
-  gen_add_syntax Module (K I)
-    (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
-    target name some_content thy;
-
 
 (* concrete syntax *)
 
-local
-
-fun zip_list (x :: xs) f g =
-  f
-  :|-- (fn y =>
-    fold_map (fn x => g |-- f >> pair x) xs
-    :|-- (fn xys => pair ((x, y) :: xys)));
-
-fun process_multi_syntax parse_thing parse_syntax change =
-  (Parse.and_list1 parse_thing
-  :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
-        (zip_list things (Scan.option parse_syntax) @{keyword "and"}) --| @{keyword ")"})))
-  >> (Toplevel.theory oo fold)
-    (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
-
-in
-
-val add_reserved = add_reserved;
-val add_const_syntax = gen_add_const_syntax (K I);
-val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
-val add_class_syntax = gen_add_class_syntax cert_class;
-val add_instance_syntax = gen_add_instance_syntax cert_inst;
-val add_include = gen_add_include (K I);
-
-val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
-val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
-val add_class_syntax_cmd = gen_add_class_syntax read_class;
-val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
-val add_include_cmd = gen_add_include Code.read_const;
-
 fun parse_args f args =
   case Scan.read Token.stopper f args
    of SOME x => x
@@ -736,11 +667,6 @@
       >> (Toplevel.theory o fold set_identifiers_cmd));
 
 val _ =
-  Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name"
-    (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
-      >> (fn (target, modlnames) => (Toplevel.theory o add_module_alias_cmd target) modlnames));
-
-val _ =
   Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols"
     (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
       Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
@@ -748,40 +674,9 @@
       >> (Toplevel.theory o fold set_printings_cmd));
 
 val _ =
-  Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
-    (process_multi_syntax Parse.term Code_Printer.parse_const_syntax
-      add_const_syntax_cmd);
-
-val _ =
-  Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
-    (process_multi_syntax Parse.type_const Code_Printer.parse_tyco_syntax
-      add_tyco_syntax_cmd);
-
-val _ =
-  Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
-    (process_multi_syntax Parse.class Parse.string
-      add_class_syntax_cmd);
-
-val _ =
-  Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
-    (process_multi_syntax parse_inst_ident (Parse.minus >> K ())
-      add_instance_syntax_cmd);
-
-val _ =
-  Outer_Syntax.command @{command_spec "code_include"}
-    "declare piece of code to be included in generated code"
-    (Parse.name -- Parse.name -- (Parse.text :|--
-      (fn "-" => Scan.succeed NONE
-        | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
-      >> (fn ((target, name), content_consts) =>
-          (Toplevel.theory o add_include_cmd target) (name, content_consts)));
-
-val _ =
   Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
     (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 
-end; (*local*)
-
 
 (** external entrance point -- for codegen tool **)
 

--- a/src/Tools/Code_Generator.thy	Sun Feb 09 19:10:12 2014 +0000
+++ b/src/Tools/Code_Generator.thy	Sun Feb 09 21:37:27 2014 +0100
@@ -8,8 +8,7 @@
 imports Pure
 keywords
   "value" "print_codeproc" "code_thms" "code_deps" :: diag and
-  "export_code" "code_identifier" "code_printing" "code_class" "code_instance" "code_type"
-    "code_const" "code_reserved" "code_include" "code_modulename"
+  "export_code" "code_identifier" "code_printing" "code_reserved"
     "code_monad" "code_reflect" :: thy_decl and
   "datatypes" "functions" "module_name" "file" "checking"
   "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"