1.1 --- a/src/Tools/Code/code_haskell.ML	Mon Aug 30 15:52:09 2010 +0900
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Mon Aug 30 09:28:02 2010 +0200
     1.3 @@ -483,7 +483,7 @@
     1.4    Code_Target.add_target
     1.5      (target, { serializer = isar_serializer, literals = literals,
     1.6        check = { env_var = "EXEC_GHC", make_destination = I,
     1.7 -        make_command = fn ghc => fn p => fn module_name =>
     1.8 +        make_command = fn ghc => fn module_name =>
     1.9            ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
    1.10    #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    1.11        brackify_infix (1, R) fxy (

     2.1 --- a/src/Tools/Code/code_ml.ML	Mon Aug 30 15:52:09 2010 +0900
     2.2 +++ b/src/Tools/Code/code_ml.ML	Mon Aug 30 09:28:02 2010 +0200
     2.3 @@ -966,11 +966,11 @@
     2.4    Code_Target.add_target
     2.5      (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
     2.6        check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
     2.7 -        make_command = fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure" } })
     2.8 +        make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
     2.9    #> Code_Target.add_target
    2.10      (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
    2.11        check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
    2.12 -        make_command = fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p } })
    2.13 +        make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
    2.14    #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    2.15        brackify_infix (1, R) fxy (
    2.16          print_typ (INFX (1, X)) ty1,

     3.1 --- a/src/Tools/Code/code_scala.ML	Mon Aug 30 15:52:09 2010 +0900
     3.2 +++ b/src/Tools/Code/code_scala.ML	Mon Aug 30 09:28:02 2010 +0200
     3.3 @@ -521,9 +521,9 @@
     3.4    Code_Target.add_target
     3.5      (target, { serializer = isar_serializer, literals = literals,
     3.6        check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
     3.7 -        make_command = fn scala_home => fn p => fn _ =>
     3.8 +        make_command = fn scala_home => fn _ =>
     3.9            "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
    3.10 -            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " " ^ File.shell_path p } })
    3.11 +            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
    3.12    #> Code_Target.add_syntax_tyco target "fun"
    3.13       (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    3.14          brackify_infix (1, R) fxy (

     4.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 15:52:09 2010 +0900
     4.2 +++ b/src/Tools/Code/code_target.ML	Mon Aug 30 09:28:02 2010 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4    type literals = Code_Printer.literals
     4.5    val add_target: string * { serializer: serializer, literals: literals,
     4.6      check: { env_var: string, make_destination: Path.T -> Path.T,
     4.7 -      make_command: string -> Path.T -> string -> string } } -> theory -> theory
     4.8 +      make_command: string -> string -> string } } -> theory -> theory
     4.9    val extend_target: string *
    4.10        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    4.11      -> theory -> theory
    4.12 @@ -116,7 +116,7 @@
    4.13  
    4.14  datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
    4.15        check: { env_var: string, make_destination: Path.T -> Path.T,
    4.16 -        make_command: string -> Path.T -> string -> string } }
    4.17 +        make_command: string -> string -> string } }
    4.18    | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    4.19  
    4.20  datatype target = Target of {
    4.21 @@ -336,7 +336,7 @@
    4.22          val destination = make_destination p;
    4.23          val _ = file destination (serialize thy target (SOME 80)
    4.24            (SOME module_name) args naming program names_cs);
    4.25 -        val cmd = make_command env_param destination module_name;
    4.26 +        val cmd = make_command env_param module_name;
    4.27        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    4.28          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    4.29          else ()