# HG changeset patch
# User wenzelm
# Date 1658406413 -7200
# Node ID b6f3db86f9c78ad6cfbcae25cec04147bd9b14a9
# Parent  83b976c3edb1c96f74a2b2ace220d39d22a44c4a
support for Java language;

diff -r 83b976c3edb1 -r b6f3db86f9c7 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jul 12 16:11:14 2022 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 21 14:26:53 2022 +0200
@@ -297,6 +297,7 @@
 
 (*Isabelle system*)
 ML_file "PIDE/protocol_command.ML";
+ML_file "System/java.ML";
 ML_file "System/scala.ML";
 ML_file "System/process_result.ML";
 ML_file "System/isabelle_system.ML";
diff -r 83b976c3edb1 -r b6f3db86f9c7 src/Pure/System/java.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/java.ML	Thu Jul 21 14:26:53 2022 +0200
@@ -0,0 +1,42 @@
+(*  Title:      Pure/System/java.ML
+    Author:     Makarius
+
+Support for Java language.
+*)
+
+signature JAVA =
+sig
+  val print_string: string -> string
+end;
+
+structure Java: JAVA =
+struct
+
+(* string literals *)
+
+local
+
+val print_str =
+  fn "\b" => "\\b"
+   | "\t" => "\\t"
+   | "\n" => "\\n"
+   | "\f" => "\\f"
+   | "\r" => "\\r"
+   | "\"" => "\\\""
+   | "\\" => "\\\\"
+   | s =>
+      let val c = ord s in
+        if c < 16 then "\\u000" ^ Int.fmt StringCvt.HEX c
+        else if c < 128 then "\\u00" ^ Int.fmt StringCvt.HEX c
+        else error ("Cannot print non-ASCII Scala string literal: " ^ quote s)
+      end;
+
+in
+
+fun print_string str =
+  quote (translate_string print_str str)
+    handle Fail _ => error ("Cannot print non-ASCII Scala string literal: " ^ quote str);
+
+end;
+
+end;