diff -r 45e4d3a855ad -r 68853347ba37 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Wed Sep 01 07:53:31 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Wed Sep 01 08:52:49 2010 +0200 @@ -488,6 +488,9 @@ end; (*local*) +val serializer : Code_Target.serializer = + Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala; + val literals = let fun char_scala c = if c = "'" then "\\'" else if c = "\"" then "\\\"" @@ -513,12 +516,9 @@ (** Isar setup **) -val isar_serializer = - Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala; - val setup = Code_Target.add_target - (target, { serializer = isar_serializer, literals = literals, + (target, { serializer = serializer, literals = literals, 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' && "