--- a/src/Pure/library.ML Tue Jun 14 20:48:41 2016 +0200
+++ b/src/Pure/library.ML Tue Jun 14 20:48:42 2016 +0200
@@ -146,6 +146,7 @@
val trim_line: string -> string
val replicate_string: int -> string -> string
val translate_string: (string -> string) -> string -> string
+ val align_right: string -> int -> string -> string
val match_string: string -> string -> bool
(*reals*)
@@ -720,6 +721,12 @@
fun translate_string f = String.translate (f o String.str);
+fun align_right c k s =
+ let
+ val _ = if size c <> 1 orelse size s > k
+ then raise Fail "align_right" else ()
+ in replicate_string (k - size s) c ^ s end;
+
(*crude matching of str against simple glob pat*)
fun match_string pat str =
let
--- a/src/Tools/Code/code_scala.ML Tue Jun 14 20:48:41 2016 +0200
+++ b/src/Tools/Code/code_scala.ML Tue Jun 14 20:48:42 2016 +0200
@@ -429,7 +429,8 @@
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
+ in if k < 32 orelse k > 126
+ then "\\u" ^ align_right "0" 4 (radixstring (8, "0", k)) else c end
fun numeral_scala k =
if ~2147483647 < k andalso k <= 2147483647
then signed_string_of_int k