# HG changeset patch
# User wenzelm
# Date 1245783951 -7200
# Node ID d78e5cff9a9ff585dd08f9364ca513a265a9a1a3
# Parent  68eccca7f51ca0793c79667e5e5f4b5321359a3c
non-public representation;

diff -r 68eccca7f51c -r d78e5cff9a9f src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Tue Jun 23 21:00:18 2009 +0200
+++ b/src/Pure/Thy/completion.scala	Tue Jun 23 21:05:51 2009 +0200
@@ -68,11 +68,11 @@
 {
   /* representation */
 
-  val words_lex = Scan.Lexicon()
-  val words_map = Map[String, String]()
+  protected val words_lex = Scan.Lexicon()
+  protected val words_map = Map[String, String]()
 
-  val abbrevs_lex = Scan.Lexicon()
-  val abbrevs_map = Map[String, (String, String)]()
+  protected val abbrevs_lex = Scan.Lexicon()
+  protected val abbrevs_map = Map[String, (String, String)]()
 
 
   /* adding stuff */