dropped legacy interfaces

--- a/doc-src/more_antiquote.ML	Mon Aug 30 18:32:40 2010 +0200
+++ b/doc-src/more_antiquote.ML	Tue Aug 31 13:08:58 2010 +0200
@@ -127,9 +127,9 @@
   (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
   (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
     let val thy = ProofContext.theory_of ctxt in
-      Code_Target.code_of thy
-        target NONE "Example" (mk_cs thy)
+      Code_Target.produce_code thy (mk_cs thy)
         (fn naming => maps (fn f => f thy naming) mk_stmtss)
+        target NONE (SOME "Example") []
       |> fst
       |> typewriter
     end);

--- a/src/Tools/Code/code_eval.ML	Mon Aug 30 18:32:40 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Tue Aug 31 13:08:58 2010 +0200
@@ -29,8 +29,8 @@
     val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
     val struct_name = if struct_name_hint = "" then eval_struct_name
       else struct_name_hint;
-    val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
-      struct_name naming program (consts' @ tycos');
+    val (ml_code, target_names) = Code_Target.produce_code_for thy
+      target NONE (SOME struct_name) [] naming program (consts' @ tycos', []);
     val (consts'', tycos'') = chop (length consts') target_names;
     val consts_map = map2 (fn const => fn NONE =>
         error ("Constant " ^ (quote o Code.string_of_const thy) const
@@ -57,8 +57,8 @@
           |> Graph.new_node (value_name,
               Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
           |> fold (curry Graph.add_edge value_name) deps;
-        val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
-          (the_default target some_target) "" naming program' [value_name];
+        val (value_code, [SOME value_name']) = Code_Target.produce_code_for thy
+          (the_default target some_target) NONE (SOME "") [] naming program ([value_name], []);
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
       in ML_Context.evaluate ctxt false reff sml_code end;

--- a/src/Tools/Code/code_ml.ML	Mon Aug 30 18:32:40 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 13:08:58 2010 +0200
@@ -8,8 +8,6 @@
 sig
   val target_SML: string
   val target_OCaml: string
-  val evaluation_code_of: theory -> string -> string
-    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
   val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
     -> Code_Printer.fixity -> 'a list -> Pretty.T option
   val setup: theory -> theory
@@ -943,13 +941,6 @@
 end; (*local*)
 
 
-(** for instrumentalization **)
-
-fun evaluation_code_of thy target struct_name =
-  Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
-    serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
-
-
 (** Isar setup **)
 
 fun isar_serializer_sml module_name =

--- a/src/Tools/Code/code_target.ML	Mon Aug 30 18:32:40 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Tue Aug 31 13:08:58 2010 +0200
@@ -42,12 +42,6 @@
     -> 'a -> int -> serialization
   val set_default_code_width: int -> theory -> theory
 
-  (*FIXME drop asap*)
-  val code_of: theory -> string -> int option -> string
-    -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
-  val serialize_custom: theory -> string * serializer -> string option
-    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
-
   val allow_abort: string -> theory -> theory
   type tyco_syntax = Code_Printer.tyco_syntax
   type const_syntax = Code_Printer.const_syntax
@@ -77,8 +71,8 @@
 fun stmt_names_of_destination (String stmt_names) = stmt_names
   | stmt_names_of_destination _ = [];
 
-fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
-  | serialization _ string pretty width (String _) = SOME (string width pretty);
+fun serialization output _ content width (File some_path) = (output width some_path content; NONE)
+  | serialization _ string content width (String _) = SOME (string width content);
 
 fun file some_path f = (f (File some_path); ());
 fun string stmt_names f = the (f (String stmt_names));
@@ -291,7 +285,7 @@
       program4 (names1, presentation_names) width
   end;
 
-fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
+fun mount_serializer thy target some_width raw_module_name args naming program names destination =
   let
     val ((targets, abortable), default_width) = Targets.get thy;
     fun collapse_hierarchy target =
@@ -306,8 +300,8 @@
           in (modify' #> modify naming, merge_target false target (data', data)) end
       end;
     val (modify, data) = collapse_hierarchy target;
-    val serializer = the_default (case the_description data
-     of Fundamental seri => #serializer seri) alt_serializer;
+    val serializer = case the_description data
+    of Fundamental seri => #serializer seri;
     val presentation_names = stmt_names_of_destination destination;
     val module_name = if null presentation_names
       then raw_module_name else SOME "Code";
@@ -332,13 +326,11 @@
 
 in
 
-fun serialize thy = mount_serializer thy NONE;
-
 fun export_code_for thy some_path target some_width some_module_name args naming program names =
-  file some_path (serialize thy target some_width some_module_name args naming program names);
+  file some_path (mount_serializer thy target some_width some_module_name args naming program names);
 
 fun produce_code_for thy target some_width some_module_name args naming program (names, selects) =
-  string selects (serialize thy target some_width some_module_name args naming program names);
+  string selects (mount_serializer thy target some_width some_module_name args naming program names);
 
 fun check_code_for thy target strict args naming program names_cs =
   let
@@ -349,7 +341,7 @@
     fun ext_check env_param p =
       let 
         val destination = make_destination p;
-        val _ = file (SOME destination) (serialize thy target (SOME 80)
+        val _ = file (SOME destination) (mount_serializer thy target (SOME 80)
           (SOME module_name) args naming program names_cs);
         val cmd = make_command env_param module_name;
       in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
@@ -363,24 +355,9 @@
     else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
   end;
 
-fun serialize_custom thy (target_name, seri) module_name naming program names =
-  mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
-  |> the;
-
 end; (* local *)
 
 
-(* code presentation *)
-
-fun code_of thy target some_width module_name cs names_stmt =
-  let
-    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
-  in
-    string (names_stmt naming)
-      (serialize thy target some_width (SOME module_name) [] naming program names_cs)
-  end;
-
-
 (* code generation *)
 
 fun transitivly_non_empty_funs thy naming program =