# HG changeset patch
# User wenzelm
# Date 1310475269 -7200
# Node ID 6dfdb70496fece6db8d1b84de03932603e89943c
# Parent  e8ba493027a3e72984b71e61a6590adab7ae4fb4
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;

diff -r e8ba493027a3 -r 6dfdb70496fe src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Tue Jul 12 14:33:08 2011 +0200
+++ b/src/Pure/General/yxml.scala	Tue Jul 12 14:54:29 2011 +0200
@@ -14,10 +14,10 @@
 {
   /* chunk markers */
 
-  private val X = '\5'
-  private val Y = '\6'
-  private val X_string = X.toString
-  private val Y_string = Y.toString
+  val X = '\5'
+  val Y = '\6'
+  val X_string = X.toString
+  val Y_string = Y.toString
 
 
   /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
diff -r e8ba493027a3 -r 6dfdb70496fe src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 14:33:08 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 14:54:29 2011 +0200
@@ -11,6 +11,30 @@
 import scala.collection.mutable
 
 
+object Outer_Syntax
+{
+  def quote_string(str: String): String =
+  {
+    val result = new StringBuilder(str.length + 10)
+    result += '"'
+    for (s <- Symbol.iterator(str)) {
+      if (s.length == 1) {
+        val c = s(0)
+        if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
+          result += '\\'
+          if (c < 10) result += '0'
+          if (c < 100) result += '0'
+          result ++= (c.asInstanceOf[Int].toString)
+        }
+        else result += c
+      }
+      else result ++= s
+    }
+    result += '"'
+    result.toString
+  }
+}
+
 class Outer_Syntax
 {
   protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))