# HG changeset patch
# User wenzelm
# Date 1218922142 -7200
# Node ID 308be7332e2524d74cf67ce2d02c6cdd5efac2b4
# Parent  beb2816f80849423241cdc32d5834912b9711c38
more private fields;

diff -r beb2816f8084 -r 308be7332e25 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Aug 16 23:28:38 2008 +0200
+++ b/src/Pure/General/symbol.scala	Sat Aug 16 23:29:02 2008 +0200
@@ -36,8 +36,8 @@
   /** Recoder tables **/
 
   class Recoder(list: List[(String, String)]) {
-    var pattern: Pattern = null
-    var table = new HashMap[String, String]
+    private var pattern: Pattern = null
+    private var table = new HashMap[String, String]
 
     def recode(text: String) = {
       val output = new StringBuffer(text.length)
@@ -69,8 +69,8 @@
     class BadSymbol(val msg: String) extends Exception
 
     private var symbols = new HashMap[String, HashMap[String, String]]
-    var decoder: Recoder = null
-    var encoder: Recoder = null
+    private var decoder: Recoder = null
+    private var encoder: Recoder = null
 
     def decode(text: String) = decoder.recode(text)
     def encode(text: String) = encoder.recode(text)