src/Pure/Tools/isabelle_syntax.scala

added append_list, encode_list;
tuned;

/*  Title:      Pure/Tools/isabelle_syntax.scala
    Author:     Makarius

Isabelle outer syntax.
*/

package isabelle

import java.util.{Properties, Enumeration}


object IsabelleSyntax {

  /* string token */

  def append_string(str: String, result: StringBuilder)
  {
    result.append("\"")
    for (c <- str) {
      if (c < 32 || c == '\\' || c == '\"') {
        result.append("\\")
        if (c < 10) result.append('0')
        if (c < 100) result.append('0')
        result.append(c.asInstanceOf[Int].toString)
      }
      else result.append(c)
    }
    result.append("\"")
  }

  def encode_string(str: String) =
  {
    val result = new StringBuilder(str.length + 20)
    append_string(str, result)
    result.toString
  }


  /* list */

  def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
    result: StringBuilder)
  {
    result.append("(")
    val elems = body.elements
    if (elems.hasNext) append_elem(elems.next, result)
    while (elems.hasNext) {
      result.append(", ")
      append_elem(elems.next, result)
    }
    result.append(")")
  }

  def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
  {
    val result = new StringBuilder(20)
    append_list(append_elem, elems, result)
    result.toString
  }


  /* properties */

  def append_properties(props: Properties, result: StringBuilder)
  {
    result.append("(")
    val names = props.propertyNames.asInstanceOf[Enumeration[String]]
    while (names.hasMoreElements) {
      val name = names.nextElement; val value = props.getProperty(name)
      append_string(name, result); result.append(" = "); append_string(value, result)
      if (names.hasMoreElements) result.append(", ")
    }
    result.append(")")
  }

  def encode_properties(props: Properties) = {
    val result = new StringBuilder(40)
    append_properties(props, result)
    result.toString
  }

}