# HG changeset patch
# User wenzelm
# Date 1245695468 -7200
# Node ID a61475260e479ac6a87b580abee02ecbc0ce4751
# Parent  19a5f1c8a8445a82caf4b7f095f043a357d66698
Lexicon: removed unused max_entry;

diff -r 19a5f1c8a844 -r a61475260e47 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Mon Jun 22 17:07:09 2009 +0200
+++ b/src/Pure/General/scan.scala	Mon Jun 22 20:31:08 2009 +0200
@@ -19,11 +19,8 @@
     private case class Tree(val branches: Map[Char, (String, Tree)])
     private val empty_tree = Tree(Map())
 
-    private def make(tree: Tree, max: Int): Lexicon =
-      new Lexicon {
-        override val main_tree = tree
-        override val max_entry = max
-      }
+    private def make(tree: Tree): Lexicon =
+      new Lexicon { override val main_tree = tree }
 
     val empty: Lexicon = new Lexicon
     def apply(strs: String*): Lexicon = (empty /: strs) ((lex, str) => lex + str)
@@ -35,7 +32,6 @@
 
     import Lexicon.Tree
     val main_tree: Tree = Lexicon.empty_tree
-    val max_entry = -1
 
 
     /* auxiliary operations */
@@ -74,7 +70,7 @@
 
     override def stringPrefix = "Lexicon"
 
-    override def isEmpty: Boolean = { max_entry < 0 }
+    override def isEmpty: Boolean = { main_tree.branches.isEmpty }
 
     def size: Int = content(main_tree, Nil).length
     def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
@@ -102,7 +98,7 @@
         } else tree
       }
       if (contains(str)) this
-      else Lexicon.make(extend(main_tree, 0), max_entry max str.length)
+      else Lexicon.make(extend(main_tree, 0))
     }
 
     def empty[A]: Set[A] = error("Undefined")