# HG changeset patch
# User wenzelm
# Date 1245181535 -7200
# Node ID cfaed41ee2c569955627482808d6a59ed7a9cc7b
# Parent  a11ea667d676368ee86dc4b758e4b85d6180e71b
added completions;
misc simplification via aux. operations;

diff -r a11ea667d676 -r cfaed41ee2c5 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Tue Jun 16 18:47:45 2009 +0200
+++ b/src/Pure/General/scan.scala	Tue Jun 16 21:45:35 2009 +0200
@@ -38,36 +38,52 @@
     val max_entry = -1
 
 
+    /* auxiliary operations */
+
+    private def content(tree: Tree, result: List[String]): List[String] =
+      (result /: tree.branches.toList) ((res, entry) =>
+        entry match { case (_, (s, tr)) =>
+          if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
+
+    private def lookup(str: CharSequence): Option[(Boolean, Tree)] =
+    {
+      val len = str.length
+      def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] =
+      {
+        if (i < len) {
+          tree.branches.get(str.charAt(i)) match {
+            case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
+            case None => None
+          }
+        } else Some(tip, tree)
+      }
+      look(main_tree, false, 0)
+    }
+
+    def completions(str: CharSequence): List[String] =
+    {
+      (lookup(str) match {
+        case Some((true, tree)) => content(tree, List(str.toString))
+        case Some((false, tree)) => content(tree, Nil)
+        case None => Nil
+      }).sort((s1, s2) => s1.length < s2.length || s1.length == s2.length && s1 <= s2)
+    }
+
+
     /* Set methods */
 
     override def stringPrefix = "Lexicon"
 
-    override def isEmpty: Boolean = (max_entry < 0)
+    override def isEmpty: Boolean = { max_entry < 0 }
 
-    private def destruct: List[String] =
-    {
-      def dest(tree: Tree, result: List[String]): List[String] =
-        (result /: tree.branches.toList) ((res, entry) =>
-          entry match { case (_, (s, tr)) =>
-            if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) })
-      dest(main_tree, Nil).sort(_ <= _)
-    }
-
-    def size: Int = destruct.length
-    def elements: Iterator[String] = destruct.elements
+    def size: Int = content(main_tree, Nil).length
+    def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
 
     def contains(str: String): Boolean =
-    {
-      val len = str.length
-      def check(tree: Tree, i: Int): Boolean =
-        i < len && {
-          tree.branches.get(str.charAt(i)) match {
-            case Some((s, tr)) => !s.isEmpty && i + 1 == len || check(tr, i + 1)
-            case None => false
-          }
-        }
-      check(main_tree, 0)
-    }
+      lookup(str) match {
+        case Some((tip, _)) => tip
+        case _ => false
+      }
 
     def +(str: String): Lexicon =
     {
@@ -104,18 +120,18 @@
         val offset = in.offset
         val len = source.length - offset
 
-        def scan(tree: Tree, i: Int, res: String): String =
+        def scan(tree: Tree, text: String, i: Int): String =
         {
           if (i < len) {
             tree.branches.get(source.charAt(offset + i)) match {
-              case Some((s, tr)) => scan(tr, i + 1, if (s.isEmpty) res else s)
-              case None => res
+              case Some((s, tr)) => scan(tr, if (s.isEmpty) text else s, i + 1)
+              case None => text
             }
-          } else res
+          } else text
         }
-        val res = scan(main_tree, 0, "")
-        if (res.isEmpty) Failure("keyword expected", in)
-        else Success(res, in.drop(res.length))
+        val text = scan(main_tree, "", 0)
+        if (text.isEmpty) Failure("keyword expected", in)
+        else Success(text, in.drop(text.length))
       }
     }.named("keyword")