space between minus sign and number for large negative number literals causes NumberFormatException at run-time
authorAndreas Lochbihler
Thu, 30 May 2013 14:37:35 +0200
changeset 5336613171b27eaca
parent 53365 ee8e3eaad24c
child 53384 3244ccb7e9db
space between minus sign and number for large negative number literals causes NumberFormatException at run-time
src/Tools/Code/code_scala.ML
     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 {