src/Tools/Code/code_target.ML
changeset 37819 000049335247
parent 37814 120c6e2d7474
child 37821 3cbb22cec751
     1.1 --- a/src/Tools/Code/code_target.ML	Wed Jul 14 14:16:12 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Wed Jul 14 14:20:47 2010 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    val code_of: theory -> string -> int option -> string
     1.5      -> string list -> (Code_Thingol.naming -> string list) -> string
     1.6    val external_check: theory -> string -> string
     1.7 -    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> Path.T -> unit
     1.8 +    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> unit
     1.9    val set_default_code_width: int -> theory -> theory
    1.10    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    1.11  
    1.12 @@ -352,10 +352,10 @@
    1.13        if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
    1.14    in union (op =) cs3 cs1 end;
    1.15  
    1.16 -fun external_check thy target env_var make_destination make_command p =
    1.17 +fun external_check thy target env_var make_destination make_command =
    1.18    let
    1.19      val env_param = getenv env_var;
    1.20 -    fun ext_check env_param =
    1.21 +    fun ext_check env_param p =
    1.22        let 
    1.23          val module_name = "Code_Test";
    1.24          val (cs, (naming, program)) =
    1.25 @@ -370,7 +370,7 @@
    1.26        end;
    1.27    in if env_param = ""
    1.28      then warning (env_var ^ " not set; skipped code check for " ^ target)
    1.29 -    else ext_check env_param
    1.30 +    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    1.31    end;
    1.32  
    1.33  fun export_code thy cs seris =