src/Pure/System/isabelle_syntax.scala

reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions

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

Isabelle outer syntax.
*/

package isabelle


object Isabelle_Syntax
{
  /* 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 + 10)
    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.iterator
    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
    append_list(append_elem, elems, result)
    result.toString
  }


  /* properties */

  def append_properties(props: List[(String, String)], result: StringBuilder)
  {
    append_list((p: (String, String), res) =>
      { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
  }

  def encode_properties(props: List[(String, String)]) =
  {
    val result = new StringBuilder
    append_properties(props, result)
    result.toString
  }
}