diff -r 645cca858c69 -r eb9fb5a4d27f src/Tools/Code/code_scala.ML --- 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 (