tuned file interface
authorhaftmann
Mon Aug 30 16:25:04 2010 +0200 (2010-08-30)
changeset 389140a49a34e5d37
parent 38913 d1d4d808be26
child 38915 026526cba0e6
tuned file interface
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 16:21:47 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Aug 30 16:25:04 2010 +0200
     1.3 @@ -31,8 +31,7 @@
     1.4      -> Code_Thingol.naming -> Code_Thingol.program -> string list
     1.5      -> string * string option list
     1.6    val the_literals: theory -> string -> literals
     1.7 -  val export: serialization -> unit
     1.8 -  val file: Path.T -> serialization -> unit
     1.9 +  val file: Path.T option -> serialization -> unit
    1.10    val string: string list -> serialization -> string
    1.11    val code_of: theory -> string -> int option -> string
    1.12      -> string list -> (Code_Thingol.naming -> string list) -> string
    1.13 @@ -65,14 +64,13 @@
    1.14  datatype destination = File of Path.T option | String of string list;
    1.15  type serialization = destination -> (string * string option list) option;
    1.16  
    1.17 -fun export f = (f (File NONE); ());
    1.18 -fun file path f = (f (File (SOME path)); ());
    1.19 +fun file some_path f = (f (File some_path); ());
    1.20  fun string stmt_names f = fst (the (f (String stmt_names)));
    1.21  
    1.22  fun stmt_names_of_destination (String stmt_names) = stmt_names
    1.23    | stmt_names_of_destination _ = [];
    1.24  
    1.25 -fun mk_serialization output _ pretty width (File path) = (output width path pretty; NONE)
    1.26 +fun mk_serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
    1.27    | mk_serialization _ string pretty width (String _) = SOME (string width pretty);
    1.28  
    1.29  
    1.30 @@ -335,7 +333,7 @@
    1.31      fun ext_check env_param p =
    1.32        let 
    1.33          val destination = make_destination p;
    1.34 -        val _ = file destination (serialize thy target (SOME 80)
    1.35 +        val _ = file (SOME destination) (serialize thy target (SOME 80)
    1.36            (SOME module_name) args naming program names_cs);
    1.37          val cmd = make_command env_param module_name;
    1.38        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.39 @@ -387,10 +385,10 @@
    1.40  fun export_code thy cs seris =
    1.41    let
    1.42      val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    1.43 -    fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
    1.44 -      else file (Path.explode dest);
    1.45 +    fun mk_destination dest = if dest = "" orelse dest = "-"
    1.46 +      then NONE else SOME (Path.explode dest);
    1.47      val _ = map (fn (((target, module), dest), args) =>
    1.48 -      (mk_seri_dest dest (serialize thy target NONE module args naming program names_cs))) seris;
    1.49 +      (file (mk_destination dest) (serialize thy target NONE module args naming program names_cs))) seris;
    1.50    in () end;
    1.51  
    1.52  fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;