tuned;

--- a/src/Tools/Code/code_scala.ML	Sun Mar 13 13:53:54 2011 +0100
+++ b/src/Tools/Code/code_scala.ML	Sun Mar 13 13:57:20 2011 +0100
@@ -64,7 +64,7 @@
               str "=>",
               print_term tyvars false some_thm vars' NOBR t
             ]
-          end 
+          end
       | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
@@ -133,7 +133,7 @@
           in brackify_block fxy
             (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
             (map print_select clauses)
-            (str "}") 
+            (str "}")
           end
       | print_case tyvars some_thm vars fxy ((_, []), _) =
           (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
@@ -273,7 +273,7 @@
                 val aux_abstr = if null auxs then [] else [enum "," "(" ")"
                   (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
                   (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
-              in 
+              in
                 concat ([str "val", print_method classparam, str "="]
                   @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
                     (const, map (IVar o SOME) auxs))
@@ -329,9 +329,11 @@
       | modify_stmt (_, Code_Thingol.Classparam _) = NONE
       | modify_stmt (_, stmt) = SOME stmt;
   in
-    Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
-      empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt,
-      cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
+    Code_Namespace.hierarchical_program labelled_name
+      { module_alias = module_alias, reserved = reserved,
+        empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
+        namify_stmt = namify_stmt, cyclic_modules = true, empty_data = [],
+        memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
   end;
 
 fun serialize_scala { labelled_name, reserved_syms, includes,
@@ -417,10 +419,12 @@
 val setup =
   Code_Target.add_target
     (target, { serializer = serializer, literals = literals,
-      check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
+      check = { env_var = "SCALA_HOME",
+        make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
         make_command = fn scala_home => fn _ =>
           "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
-            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
+            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac"))
+            ^ " ROOT.scala" } })
   #> Code_Target.add_tyco_syntax target "fun"
      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
         brackify_infix (1, R) fxy (

--- a/src/Tools/Code/code_target.ML	Sun Mar 13 13:53:54 2011 +0100
+++ b/src/Tools/Code/code_target.ML	Sun Mar 13 13:57:20 2011 +0100
@@ -393,7 +393,7 @@
     val { env_var, make_destination, make_command } =
       (#check o the_fundamental thy) target;
     val env_param = getenv env_var;
-    fun ext_check env_param p =
+    fun ext_check p =
       let 
         val destination = make_destination p;
         val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
@@ -407,7 +407,7 @@
     then if strict
       then error (env_var ^ " not set; cannot check code for " ^ target)
       else warning (env_var ^ " not set; skipped checking code for " ^ target)
-    else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
+    else Isabelle_System.with_tmp_dir "Code_Test" ext_check
   end;
 
 fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) =