src/Tools/Code/code_scala.ML
changeset 34888 460ec1a99aa2
parent 34308 394fc3cce915
child 34900 9b12b0824bfe
     1.1 --- a/src/Tools/Code/code_scala.ML	Wed Jan 13 08:56:16 2010 +0100
     1.2 +++ b/src/Tools/Code/code_scala.ML	Wed Jan 13 08:56:16 2010 +0100
     1.3 @@ -409,7 +409,7 @@
     1.4    literal_string = quote o translate_string char_scala,
     1.5    literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
     1.6      else Library.enclose "(" ")" (signed_string_of_int k),
     1.7 -  literal_list = fn ps => Pretty.block [str "List", enum "," "(" ")" ps],
     1.8 +  literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
     1.9    infix_cons = (6, "::")
    1.10  } end;
    1.11  
    1.12 @@ -436,7 +436,7 @@
    1.13        "true", "type", "val", "var", "while", "with"
    1.14      ]
    1.15    #> fold (Code_Target.add_reserved target) [
    1.16 -      "error", "apply", "List"
    1.17 +      "error", "apply", "List", "Nil"
    1.18      ];
    1.19  
    1.20  end; (*struct*)