# HG changeset patch
# User haftmann
# Date 1263369376 -3600
# Node ID 460ec1a99aa218e491f7a49a02fd5e8eec37680a
# Parent  31209fb24176500dd69f937f2a86eec51f3af0fd
being more accurate wrt. list syntax

diff -r 31209fb24176 -r 460ec1a99aa2 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Jan 13 08:56:16 2010 +0100
+++ b/src/Tools/Code/code_scala.ML	Wed Jan 13 08:56:16 2010 +0100
@@ -409,7 +409,7 @@
   literal_string = quote o translate_string char_scala,
   literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
     else Library.enclose "(" ")" (signed_string_of_int k),
-  literal_list = fn ps => Pretty.block [str "List", enum "," "(" ")" ps],
+  literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   infix_cons = (6, "::")
 } end;
 
@@ -436,7 +436,7 @@
       "true", "type", "val", "var", "while", "with"
     ]
   #> fold (Code_Target.add_reserved target) [
-      "error", "apply", "List"
+      "error", "apply", "List", "Nil"
     ];
 
 end; (*struct*)