# HG changeset patch
# User wenzelm
# Date 1232305501 -3600
# Node ID 5b21c79785b03686413217cd7e0294836f390700
# Parent  95e469919c3e46229e7a81650bbc5f6d14ef603c
added append_list, encode_list;
tuned;

diff -r 95e469919c3e -r 5b21c79785b0 src/Pure/Tools/isabelle_syntax.scala
--- a/src/Pure/Tools/isabelle_syntax.scala	Sun Jan 18 16:42:43 2009 +0100
+++ b/src/Pure/Tools/isabelle_syntax.scala	Sun Jan 18 20:05:01 2009 +0100
@@ -13,7 +13,8 @@
 
   /* string token */
 
-  def append_string(str: String, result: StringBuilder) = {
+  def append_string(str: String, result: StringBuilder)
+  {
     result.append("\"")
     for (c <- str) {
       if (c < 32 || c == '\\' || c == '\"') {
@@ -27,16 +28,41 @@
     result.append("\"")
   }
 
-  def encode_string(str: String) = {
+  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) = {
+  def append_properties(props: Properties, result: StringBuilder)
+  {
     result.append("(")
     val names = props.propertyNames.asInstanceOf[Enumeration[String]]
     while (names.hasMoreElements) {