1.1 --- a/src/Tools/Code/code_target.ML	Sun Mar 13 13:57:20 2011 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Sun Mar 13 14:51:38 2011 +0100
     1.3 @@ -35,8 +35,8 @@
     1.4    type serializer
     1.5    type literals = Code_Printer.literals
     1.6    val add_target: string * { serializer: serializer, literals: literals,
     1.7 -    check: { env_var: string, make_destination: Path.T -> Path.T,
     1.8 -      make_command: string -> string -> string } } -> theory -> theory
     1.9 +    check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
    1.10 +    -> theory -> theory
    1.11    val extend_target: string *
    1.12        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    1.13      -> theory -> theory
    1.14 @@ -129,7 +129,7 @@
    1.15  datatype description = Fundamental of { serializer: serializer,
    1.16        literals: literals,
    1.17        check: { env_var: string, make_destination: Path.T -> Path.T,
    1.18 -        make_command: string -> string -> string } }
    1.19 +        make_command: string -> string } }
    1.20    | Extension of string *
    1.21        (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    1.22  
    1.23 @@ -392,18 +392,17 @@
    1.24      val module_name = "Code";
    1.25      val { env_var, make_destination, make_command } =
    1.26        (#check o the_fundamental thy) target;
    1.27 -    val env_param = getenv env_var;
    1.28      fun ext_check p =
    1.29        let 
    1.30          val destination = make_destination p;
    1.31          val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
    1.32            module_name args naming program names_cs);
    1.33 -        val cmd = make_command env_param module_name;
    1.34 +        val cmd = make_command module_name;
    1.35        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.36          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    1.37          else ()
    1.38        end;
    1.39 -  in if env_param = ""
    1.40 +  in if getenv env_var = ""
    1.41      then if strict
    1.42        then error (env_var ^ " not set; cannot check code for " ^ target)
    1.43        else warning (env_var ^ " not set; skipped checking code for " ^ target)