# HG changeset patch
# User wenzelm
# Date 1319319781 -7200
# Node ID 6de58d947e575244286ac6857b10fe17e97b29f8
# Parent  12913296be794a5f313ece2006bcdae3fe03b253
class Lexicon as abstract datatype;

diff -r 12913296be79 -r 6de58d947e57 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sat Oct 22 23:30:02 2011 +0200
+++ b/src/Pure/General/scan.scala	Sat Oct 22 23:43:01 2011 +0200
@@ -32,19 +32,19 @@
 
   object Lexicon
   {
-    protected case class Tree(val branches: Map[Char, (String, Tree)])
+    /* representation */
+
+    sealed case class Tree(val branches: Map[Char, (String, Tree)])
     private val empty_tree = Tree(Map())
 
-    val empty: Lexicon = new Lexicon
+    val empty: Lexicon = new Lexicon(empty_tree)
     def apply(elems: String*): Lexicon = empty ++ elems
   }
 
-  class Lexicon extends Addable[String, Lexicon] with RegexParsers
+  class Lexicon private(private val main_tree: Lexicon.Tree)
+    extends Addable[String, Lexicon] with RegexParsers
   {
-    /* representation */
-
     import Lexicon.Tree
-    protected val main_tree: Tree = Lexicon.empty_tree
 
 
     /* auxiliary operations */
@@ -116,7 +116,7 @@
           }
           else tree
         val old = this
-        new Lexicon { override val main_tree = extend(old.main_tree, 0) }
+        new Lexicon(extend(old.main_tree, 0))
       }