added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
authorwenzelm
Tue Jul 12 14:54:29 2011 +0200 (2011-07-12)
changeset 437746dfdb70496fe
parent 43773 e8ba493027a3
child 43775 b361c7d184e7
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
src/Pure/General/yxml.scala
src/Pure/Isar/outer_syntax.scala
     1.1 --- a/src/Pure/General/yxml.scala	Tue Jul 12 14:33:08 2011 +0200
     1.2 +++ b/src/Pure/General/yxml.scala	Tue Jul 12 14:54:29 2011 +0200
     1.3 @@ -14,10 +14,10 @@
     1.4  {
     1.5    /* chunk markers */
     1.6  
     1.7 -  private val X = '\5'
     1.8 -  private val Y = '\6'
     1.9 -  private val X_string = X.toString
    1.10 -  private val Y_string = Y.toString
    1.11 +  val X = '\5'
    1.12 +  val Y = '\6'
    1.13 +  val X_string = X.toString
    1.14 +  val Y_string = Y.toString
    1.15  
    1.16  
    1.17    /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 14:33:08 2011 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 14:54:29 2011 +0200
     2.3 @@ -11,6 +11,30 @@
     2.4  import scala.collection.mutable
     2.5  
     2.6  
     2.7 +object Outer_Syntax
     2.8 +{
     2.9 +  def quote_string(str: String): String =
    2.10 +  {
    2.11 +    val result = new StringBuilder(str.length + 10)
    2.12 +    result += '"'
    2.13 +    for (s <- Symbol.iterator(str)) {
    2.14 +      if (s.length == 1) {
    2.15 +        val c = s(0)
    2.16 +        if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
    2.17 +          result += '\\'
    2.18 +          if (c < 10) result += '0'
    2.19 +          if (c < 100) result += '0'
    2.20 +          result ++= (c.asInstanceOf[Int].toString)
    2.21 +        }
    2.22 +        else result += c
    2.23 +      }
    2.24 +      else result ++= s
    2.25 +    }
    2.26 +    result += '"'
    2.27 +    result.toString
    2.28 +  }
    2.29 +}
    2.30 +
    2.31  class Outer_Syntax
    2.32  {
    2.33    protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))