src/Pure/Tools/isabelle_syntax.scala
changeset 29552 5b21c79785b0
parent 29140 e7ac5bb20aed
child 29571 ba0cf984e593
     1.1 --- a/src/Pure/Tools/isabelle_syntax.scala	Sun Jan 18 16:42:43 2009 +0100
     1.2 +++ b/src/Pure/Tools/isabelle_syntax.scala	Sun Jan 18 20:05:01 2009 +0100
     1.3 @@ -13,7 +13,8 @@
     1.4  
     1.5    /* string token */
     1.6  
     1.7 -  def append_string(str: String, result: StringBuilder) = {
     1.8 +  def append_string(str: String, result: StringBuilder)
     1.9 +  {
    1.10      result.append("\"")
    1.11      for (c <- str) {
    1.12        if (c < 32 || c == '\\' || c == '\"') {
    1.13 @@ -27,16 +28,41 @@
    1.14      result.append("\"")
    1.15    }
    1.16  
    1.17 -  def encode_string(str: String) = {
    1.18 +  def encode_string(str: String) =
    1.19 +  {
    1.20      val result = new StringBuilder(str.length + 20)
    1.21      append_string(str, result)
    1.22      result.toString
    1.23    }
    1.24  
    1.25  
    1.26 +  /* list */
    1.27 +
    1.28 +  def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
    1.29 +    result: StringBuilder)
    1.30 +  {
    1.31 +    result.append("(")
    1.32 +    val elems = body.elements
    1.33 +    if (elems.hasNext) append_elem(elems.next, result)
    1.34 +    while (elems.hasNext) {
    1.35 +      result.append(", ")
    1.36 +      append_elem(elems.next, result)
    1.37 +    }
    1.38 +    result.append(")")
    1.39 +  }
    1.40 +
    1.41 +  def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
    1.42 +  {
    1.43 +    val result = new StringBuilder(20)
    1.44 +    append_list(append_elem, elems, result)
    1.45 +    result.toString
    1.46 +  }
    1.47 +
    1.48 +
    1.49    /* properties */
    1.50  
    1.51 -  def append_properties(props: Properties, result: StringBuilder) = {
    1.52 +  def append_properties(props: Properties, result: StringBuilder)
    1.53 +  {
    1.54      result.append("(")
    1.55      val names = props.propertyNames.asInstanceOf[Enumeration[String]]
    1.56      while (names.hasMoreElements) {