src/Tools/Code/code_target.ML
changeset 38921 15f8cffdbf5d
parent 38918 48d62f237944
child 38923 79d7f2b4cf71
     1.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 18:32:40 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 13:08:58 2010 +0200
     1.3 @@ -42,12 +42,6 @@
     1.4      -> 'a -> int -> serialization
     1.5    val set_default_code_width: int -> theory -> theory
     1.6  
     1.7 -  (*FIXME drop asap*)
     1.8 -  val code_of: theory -> string -> int option -> string
     1.9 -    -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
    1.10 -  val serialize_custom: theory -> string * serializer -> string option
    1.11 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    1.12 -
    1.13    val allow_abort: string -> theory -> theory
    1.14    type tyco_syntax = Code_Printer.tyco_syntax
    1.15    type const_syntax = Code_Printer.const_syntax
    1.16 @@ -77,8 +71,8 @@
    1.17  fun stmt_names_of_destination (String stmt_names) = stmt_names
    1.18    | stmt_names_of_destination _ = [];
    1.19  
    1.20 -fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
    1.21 -  | serialization _ string pretty width (String _) = SOME (string width pretty);
    1.22 +fun serialization output _ content width (File some_path) = (output width some_path content; NONE)
    1.23 +  | serialization _ string content width (String _) = SOME (string width content);
    1.24  
    1.25  fun file some_path f = (f (File some_path); ());
    1.26  fun string stmt_names f = the (f (String stmt_names));
    1.27 @@ -291,7 +285,7 @@
    1.28        program4 (names1, presentation_names) width
    1.29    end;
    1.30  
    1.31 -fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
    1.32 +fun mount_serializer thy target some_width raw_module_name args naming program names destination =
    1.33    let
    1.34      val ((targets, abortable), default_width) = Targets.get thy;
    1.35      fun collapse_hierarchy target =
    1.36 @@ -306,8 +300,8 @@
    1.37            in (modify' #> modify naming, merge_target false target (data', data)) end
    1.38        end;
    1.39      val (modify, data) = collapse_hierarchy target;
    1.40 -    val serializer = the_default (case the_description data
    1.41 -     of Fundamental seri => #serializer seri) alt_serializer;
    1.42 +    val serializer = case the_description data
    1.43 +    of Fundamental seri => #serializer seri;
    1.44      val presentation_names = stmt_names_of_destination destination;
    1.45      val module_name = if null presentation_names
    1.46        then raw_module_name else SOME "Code";
    1.47 @@ -332,13 +326,11 @@
    1.48  
    1.49  in
    1.50  
    1.51 -fun serialize thy = mount_serializer thy NONE;
    1.52 -
    1.53  fun export_code_for thy some_path target some_width some_module_name args naming program names =
    1.54 -  file some_path (serialize thy target some_width some_module_name args naming program names);
    1.55 +  file some_path (mount_serializer thy target some_width some_module_name args naming program names);
    1.56  
    1.57  fun produce_code_for thy target some_width some_module_name args naming program (names, selects) =
    1.58 -  string selects (serialize thy target some_width some_module_name args naming program names);
    1.59 +  string selects (mount_serializer thy target some_width some_module_name args naming program names);
    1.60  
    1.61  fun check_code_for thy target strict args naming program names_cs =
    1.62    let
    1.63 @@ -349,7 +341,7 @@
    1.64      fun ext_check env_param p =
    1.65        let 
    1.66          val destination = make_destination p;
    1.67 -        val _ = file (SOME destination) (serialize thy target (SOME 80)
    1.68 +        val _ = file (SOME destination) (mount_serializer thy target (SOME 80)
    1.69            (SOME module_name) args naming program names_cs);
    1.70          val cmd = make_command env_param module_name;
    1.71        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.72 @@ -363,24 +355,9 @@
    1.73      else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    1.74    end;
    1.75  
    1.76 -fun serialize_custom thy (target_name, seri) module_name naming program names =
    1.77 -  mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
    1.78 -  |> the;
    1.79 -
    1.80  end; (* local *)
    1.81  
    1.82  
    1.83 -(* code presentation *)
    1.84 -
    1.85 -fun code_of thy target some_width module_name cs names_stmt =
    1.86 -  let
    1.87 -    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    1.88 -  in
    1.89 -    string (names_stmt naming)
    1.90 -      (serialize thy target some_width (SOME module_name) [] naming program names_cs)
    1.91 -  end;
    1.92 -
    1.93 -
    1.94  (* code generation *)
    1.95  
    1.96  fun transitivly_non_empty_funs thy naming program =