# HG changeset patch
# User haftmann
# Date 1275381054 -7200
# Node ID f4d3c929c526d88d96925281019102f664b670b2
# Parent  5226259b6fa24114a3a09e4e6785471b95ab1c46
corrected printing of characters

diff -r 5226259b6fa2 -r f4d3c929c526 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Tue Jun 01 10:30:53 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Tue Jun 01 10:30:54 2010 +0200
@@ -400,10 +400,11 @@
   end;
 
 val literals = let
-  fun char_scala c =
-    let
-      val s = ML_Syntax.print_char c;
-    in if s = "'" then "\\'" else s end;
+  fun char_scala c = if c = "'" then "\\'"
+    else if c = "\"" then "\\\""
+    else if c = "\\" then "\\\\"
+    else let val k = ord c
+    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))