75682
|
1 |
(* Title: Pure/System/java.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Support for Java language.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature JAVA =
|
|
8 |
sig
|
|
9 |
val print_string: string -> string
|
|
10 |
end;
|
|
11 |
|
|
12 |
structure Java: JAVA =
|
|
13 |
struct
|
|
14 |
|
|
15 |
(* string literals *)
|
|
16 |
|
|
17 |
local
|
|
18 |
|
|
19 |
val print_str =
|
|
20 |
fn "\b" => "\\b"
|
|
21 |
| "\t" => "\\t"
|
|
22 |
| "\n" => "\\n"
|
|
23 |
| "\f" => "\\f"
|
|
24 |
| "\r" => "\\r"
|
|
25 |
| "\"" => "\\\""
|
|
26 |
| "\\" => "\\\\"
|
|
27 |
| s =>
|
|
28 |
let val c = ord s in
|
75964
|
29 |
if 32 < c andalso c < 127 andalso c <> 34 andalso c <> 92 then s
|
|
30 |
else if c < 16 then "\\u000" ^ Int.fmt StringCvt.HEX c
|
75682
|
31 |
else if c < 128 then "\\u00" ^ Int.fmt StringCvt.HEX c
|
75684
|
32 |
else error ("Cannot print non-ASCII Java/Scala string literal: " ^ quote s)
|
75682
|
33 |
end;
|
|
34 |
|
|
35 |
in
|
|
36 |
|
|
37 |
fun print_string str =
|
|
38 |
quote (translate_string print_str str)
|
75684
|
39 |
handle Fail _ => error ("Cannot print non-ASCII Java/Scala string literal: " ^ quote str);
|
75682
|
40 |
|
|
41 |
end;
|
|
42 |
|
|
43 |
end;
|