# HG changeset patch
# User wenzelm
# Date 1232471216 -3600
# Node ID ba0cf984e59368efaeaea5ce01725d9e75b7b4f7
# Parent  10fca82e688a7625e953031863b90d0bf0aef659
replaced java.util.Properties by plain association list;
tuned;

diff -r 10fca82e688a -r ba0cf984e593 src/Pure/Tools/isabelle_syntax.scala
--- a/src/Pure/Tools/isabelle_syntax.scala	Tue Jan 20 18:05:21 2009 +0100
+++ b/src/Pure/Tools/isabelle_syntax.scala	Tue Jan 20 18:06:56 2009 +0100
@@ -6,8 +6,6 @@
 
 package isabelle
 
-import java.util.{Properties, Enumeration}
-
 
 object IsabelleSyntax {
 
@@ -30,7 +28,7 @@
 
   def encode_string(str: String) =
   {
-    val result = new StringBuilder(str.length + 20)
+    val result = new StringBuilder(str.length + 10)
     append_string(str, result)
     result.toString
   }
@@ -53,7 +51,7 @@
 
   def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
   {
-    val result = new StringBuilder(20)
+    val result = new StringBuilder
     append_list(append_elem, elems, result)
     result.toString
   }
@@ -61,22 +59,16 @@
 
   /* properties */
 
-  def append_properties(props: Properties, result: StringBuilder)
+  def append_properties(props: List[(String, String)], 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(")")
+    append_list((p: (String, String), res) =>
+      { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
   }
 
-  def encode_properties(props: Properties) = {
-    val result = new StringBuilder(40)
+  def encode_properties(props: List[(String, String)]) =
+  {
+    val result = new StringBuilder
     append_properties(props, result)
     result.toString
   }
-
 }