check without explicit path
authorhaftmann
Wed Jul 14 14:20:47 2010 +0200 (2010-07-14)
changeset 37819000049335247
parent 37818 dd65033fed78
child 37820 ffaca9167c16
check without explicit path
src/HOL/Codegenerator_Test/Generate.thy
src/HOL/Codegenerator_Test/Generate_Pretty.thy
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 14:16:12 2010 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 14:20:47 2010 +0200
     1.3 @@ -15,15 +15,15 @@
     1.4  *}
     1.5  
     1.6  export_code "*" in SML module_name Code_Test file -
     1.7 -ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
     1.8 +ML {* Code_ML.check_SML @{theory} *}
     1.9  
    1.10  export_code "*" in OCaml module_name Code_Test file -
    1.11 -ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
    1.12 +ML {* Code_ML.check_OCaml @{theory} *}
    1.13  
    1.14  export_code "*" in Haskell module_name Code_Test file -
    1.15 -ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
    1.16 +ML {* Code_Haskell.check @{theory} *}
    1.17  
    1.18  export_code "*" in Scala module_name Code_Test file -
    1.19 -ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
    1.20 +ML {* Code_Scala.check @{theory} *}
    1.21  
    1.22  end
     2.1 --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 14:16:12 2010 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 14:20:47 2010 +0200
     2.3 @@ -20,15 +20,15 @@
     2.4  *}
     2.5  
     2.6  export_code "*" in SML module_name Code_Test file -
     2.7 -ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
     2.8 +ML {* Code_ML.check_SML @{theory} *}
     2.9  
    2.10  export_code "*" in OCaml module_name Code_Test file -
    2.11 -ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
    2.12 +ML {* Code_ML.check_OCaml @{theory} *}
    2.13  
    2.14  export_code "*" in Haskell module_name Code_Test file -
    2.15 -ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
    2.16 +ML {* Code_Haskell.check @{theory} *}
    2.17  
    2.18  export_code "*" in Scala module_name Code_Test file -
    2.19 -ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
    2.20 +ML {* Code_Scala.check @{theory} *}
    2.21  
    2.22  end
     3.1 --- a/src/Tools/Code/code_haskell.ML	Wed Jul 14 14:16:12 2010 +0200
     3.2 +++ b/src/Tools/Code/code_haskell.ML	Wed Jul 14 14:20:47 2010 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  signature CODE_HASKELL =
     3.5  sig
     3.6    val target: string
     3.7 -  val check: theory -> Path.T -> unit
     3.8 +  val check: theory -> unit
     3.9    val setup: theory -> theory
    3.10  end;
    3.11  
     4.1 --- a/src/Tools/Code/code_ml.ML	Wed Jul 14 14:16:12 2010 +0200
     4.2 +++ b/src/Tools/Code/code_ml.ML	Wed Jul 14 14:20:47 2010 +0200
     4.3 @@ -12,8 +12,8 @@
     4.4      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
     4.5    val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
     4.6      -> Code_Printer.fixity -> 'a list -> Pretty.T option
     4.7 -  val check_SML: theory -> Path.T -> unit
     4.8 -  val check_OCaml: theory -> Path.T -> unit
     4.9 +  val check_SML: theory -> unit
    4.10 +  val check_OCaml: theory -> unit
    4.11    val setup: theory -> theory
    4.12  end;
    4.13  
     5.1 --- a/src/Tools/Code/code_scala.ML	Wed Jul 14 14:16:12 2010 +0200
     5.2 +++ b/src/Tools/Code/code_scala.ML	Wed Jul 14 14:20:47 2010 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  signature CODE_SCALA =
     5.5  sig
     5.6    val target: string
     5.7 -  val check: theory -> Path.T -> unit
     5.8 +  val check: theory -> unit
     5.9    val setup: theory -> theory
    5.10  end;
    5.11  
     6.1 --- a/src/Tools/Code/code_target.ML	Wed Jul 14 14:16:12 2010 +0200
     6.2 +++ b/src/Tools/Code/code_target.ML	Wed Jul 14 14:20:47 2010 +0200
     6.3 @@ -35,7 +35,7 @@
     6.4    val code_of: theory -> string -> int option -> string
     6.5      -> string list -> (Code_Thingol.naming -> string list) -> string
     6.6    val external_check: theory -> string -> string
     6.7 -    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> Path.T -> unit
     6.8 +    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> unit
     6.9    val set_default_code_width: int -> theory -> theory
    6.10    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    6.11  
    6.12 @@ -352,10 +352,10 @@
    6.13        if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
    6.14    in union (op =) cs3 cs1 end;
    6.15  
    6.16 -fun external_check thy target env_var make_destination make_command p =
    6.17 +fun external_check thy target env_var make_destination make_command =
    6.18    let
    6.19      val env_param = getenv env_var;
    6.20 -    fun ext_check env_param =
    6.21 +    fun ext_check env_param p =
    6.22        let 
    6.23          val module_name = "Code_Test";
    6.24          val (cs, (naming, program)) =
    6.25 @@ -370,7 +370,7 @@
    6.26        end;
    6.27    in if env_param = ""
    6.28      then warning (env_var ^ " not set; skipped code check for " ^ target)
    6.29 -    else ext_check env_param
    6.30 +    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    6.31    end;
    6.32  
    6.33  fun export_code thy cs seris =