--- a/src/Pure/General/symbol.scala Sun Mar 06 11:59:35 2016 +0100
+++ b/src/Pure/General/symbol.scala Sun Mar 06 13:19:19 2016 +0100
@@ -54,6 +54,12 @@
def is_ascii_identifier(s: String): Boolean =
s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig)
+ def ascii(c: Char): Symbol =
+ {
+ if (c > 127) error("Non-ASCII character: " + quote(c.toString))
+ else char_symbols(c.toInt)
+ }
+
/* symbol matching */
--- a/src/Pure/ML/ml_syntax.ML Sun Mar 06 11:59:35 2016 +0100
+++ b/src/Pure/ML/ml_syntax.ML Sun Mar 06 13:19:19 2016 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/ML/ml_syntax.ML
Author: Makarius
-Basic ML syntax operations.
+Concrete ML syntax for basic values.
*)
signature ML_SYNTAX =
@@ -59,20 +59,25 @@
fun print_option f NONE = "NONE"
| print_option f (SOME x) = "SOME (" ^ f x ^ ")";
+fun print_chr s =
+ if Symbol.is_char s then
+ (case ord s of
+ 34 => "\\\""
+ | 92 => "\\\\"
+ | 9 => "\\t"
+ | 10 => "\\n"
+ | 11 => "\\f"
+ | 13 => "\\r"
+ | c =>
+ if c < 32 then "\\^" ^ chr (c + 64)
+ else if c < 127 then s
+ else "\\" ^ string_of_int c)
+ else error ("Bad character: " ^ quote s);
+
fun print_char s =
- if not (Symbol.is_char s) then s
- else if s = "\"" then "\\\""
- else if s = "\\" then "\\\\"
- else if s = "\t" then "\\t"
- else if s = "\n" then "\\n"
- else if s = "\f" then "\\f"
- else if s = "\r" then "\\r"
- else
- let val c = ord s in
- if c < 32 then "\\^" ^ chr (c + ord "@")
- else if c < 127 then s
- else "\\" ^ string_of_int c
- end;
+ if Symbol.is_char s then print_chr s
+ else if Symbol.is_utf8 s then translate_string print_chr s
+ else s;
val print_string = quote o implode o map print_char o Symbol.explode;
val print_strings = print_list print_string;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_syntax.scala Sun Mar 06 13:19:19 2016 +0100
@@ -0,0 +1,36 @@
+/* Title: Pure/ML/ml_syntax.scala
+ Author: Makarius
+
+Concrete ML syntax for basic values.
+*/
+
+package isabelle
+
+
+object ML_Syntax
+{
+ private def print_chr(c: Byte): String =
+ c match {
+ case 34 => "\\\""
+ case 92 => "\\\\"
+ case 9 => "\\t"
+ case 10 => "\\n"
+ case 12 => "\\f"
+ case 13 => "\\r"
+ case _ =>
+ if (c < 0) "\\" + Library.signed_string_of_int(256 + c)
+ else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar))
+ else if (c < 127) Symbol.ascii(c.toChar)
+ else "\\" + Library.signed_string_of_int(c)
+ }
+
+ def print_char(s: Symbol.Symbol): String =
+ if (s.startsWith("\\<")) s
+ else UTF8.bytes(s).iterator.map(print_chr(_)).mkString
+
+ def print_string(str: String): String =
+ quote(Symbol.iterator(str).map(print_char(_)).mkString)
+
+ def print_string_raw(str: String): String =
+ quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
+}
--- a/src/Pure/build-jars Sun Mar 06 11:59:35 2016 +0100
+++ b/src/Pure/build-jars Sun Mar 06 13:19:19 2016 +0100
@@ -55,6 +55,7 @@
Isar/parse.scala
Isar/token.scala
ML/ml_lex.scala
+ ML/ml_syntax.scala
PIDE/batch_session.scala
PIDE/command.scala
PIDE/command_span.scala