# HG changeset patch
# User haftmann
# Date 1279110047 -7200
# Node ID 0000493352471960616e1db29049cb3ed6f83870
# Parent  dd65033fed78dbaa892b206b3363532bacabfc62
check without explicit path

diff -r dd65033fed78 -r 000049335247 src/HOL/Codegenerator_Test/Generate.thy
--- a/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 14:16:12 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 14:20:47 2010 +0200
@@ -15,15 +15,15 @@
 *}
 
 export_code "*" in SML module_name Code_Test file -
-ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
+ML {* Code_ML.check_SML @{theory} *}
 
 export_code "*" in OCaml module_name Code_Test file -
-ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
+ML {* Code_ML.check_OCaml @{theory} *}
 
 export_code "*" in Haskell module_name Code_Test file -
-ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
+ML {* Code_Haskell.check @{theory} *}
 
 export_code "*" in Scala module_name Code_Test file -
-ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
+ML {* Code_Scala.check @{theory} *}
 
 end
diff -r dd65033fed78 -r 000049335247 src/HOL/Codegenerator_Test/Generate_Pretty.thy
--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 14:16:12 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 14:20:47 2010 +0200
@@ -20,15 +20,15 @@
 *}
 
 export_code "*" in SML module_name Code_Test file -
-ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
+ML {* Code_ML.check_SML @{theory} *}
 
 export_code "*" in OCaml module_name Code_Test file -
-ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
+ML {* Code_ML.check_OCaml @{theory} *}
 
 export_code "*" in Haskell module_name Code_Test file -
-ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
+ML {* Code_Haskell.check @{theory} *}
 
 export_code "*" in Scala module_name Code_Test file -
-ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
+ML {* Code_Scala.check @{theory} *}
 
 end
diff -r dd65033fed78 -r 000049335247 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Wed Jul 14 14:16:12 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Jul 14 14:20:47 2010 +0200
@@ -7,7 +7,7 @@
 signature CODE_HASKELL =
 sig
   val target: string
-  val check: theory -> Path.T -> unit
+  val check: theory -> unit
   val setup: theory -> theory
 end;
 
diff -r dd65033fed78 -r 000049335247 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Wed Jul 14 14:16:12 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Wed Jul 14 14:20:47 2010 +0200
@@ -12,8 +12,8 @@
     -> 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 check_SML: theory -> Path.T -> unit
-  val check_OCaml: theory -> Path.T -> unit
+  val check_SML: theory -> unit
+  val check_OCaml: theory -> unit
   val setup: theory -> theory
 end;
 
diff -r dd65033fed78 -r 000049335247 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Jul 14 14:16:12 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Jul 14 14:20:47 2010 +0200
@@ -7,7 +7,7 @@
 signature CODE_SCALA =
 sig
   val target: string
-  val check: theory -> Path.T -> unit
+  val check: theory -> unit
   val setup: theory -> theory
 end;
 
diff -r dd65033fed78 -r 000049335247 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Jul 14 14:16:12 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Wed Jul 14 14:20:47 2010 +0200
@@ -35,7 +35,7 @@
   val code_of: theory -> string -> int option -> string
     -> string list -> (Code_Thingol.naming -> string list) -> string
   val external_check: theory -> string -> string
-    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> Path.T -> unit
+    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> unit
   val set_default_code_width: int -> theory -> theory
   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
 
@@ -352,10 +352,10 @@
       if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
   in union (op =) cs3 cs1 end;
 
-fun external_check thy target env_var make_destination make_command p =
+fun external_check thy target env_var make_destination make_command =
   let
     val env_param = getenv env_var;
-    fun ext_check env_param =
+    fun ext_check env_param p =
       let 
         val module_name = "Code_Test";
         val (cs, (naming, program)) =
@@ -370,7 +370,7 @@
       end;
   in if env_param = ""
     then warning (env_var ^ " not set; skipped code check for " ^ target)
-    else ext_check env_param
+    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
   end;
 
 fun export_code thy cs seris =