# HG changeset patch # User wenzelm # Date 1369929158 -7200 # Node ID 3244ccb7e9db5e35601d9437c288b313ea770a74 # Parent 13171b27eacaa7ba4a6e30c26b8d6b6d695b3167# Parent 54c0d4128b30fa5e0d00fc3b6717bbd6995a7692 merged diff -r 54c0d4128b30 -r 3244ccb7e9db src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Thu May 30 17:26:01 2013 +0200 +++ b/src/Tools/Code/code_scala.ML Thu May 30 17:52:38 2013 +0200 @@ -392,7 +392,7 @@ in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end fun numeral_scala k = if k < 0 then if k > ~ 2147483647 then "- " ^ string_of_int (~ k) - else quote ("- " ^ string_of_int (~ k)) + else quote ("-" ^ string_of_int (~ k)) else if k <= 2147483647 then string_of_int k else quote (string_of_int k) in Literals {