space between minus sign and number for large negative number literals causes NumberFormatException at run-time
1.1 --- a/src/Tools/Code/code_scala.ML Thu May 30 08:27:51 2013 +0200
1.2 +++ b/src/Tools/Code/code_scala.ML Thu May 30 14:37:35 2013 +0200
1.3 @@ -392,7 +392,7 @@
1.4 in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
1.5 fun numeral_scala k = if k < 0
1.6 then if k > ~ 2147483647 then "- " ^ string_of_int (~ k)
1.7 - else quote ("- " ^ string_of_int (~ k))
1.8 + else quote ("-" ^ string_of_int (~ k))
1.9 else if k <= 2147483647 then string_of_int k
1.10 else quote (string_of_int k)
1.11 in Literals {