1.1 --- a/src/Pure/Thy/completion.scala	Sun Dec 20 15:42:40 2009 +0100
     1.2 +++ b/src/Pure/Thy/completion.scala	Sun Dec 20 15:44:07 2009 +0100
     1.3 @@ -12,34 +12,6 @@
     1.4  
     1.5  private object Completion
     1.6  {
     1.7 -  /** String/CharSequence utilities */
     1.8 -
     1.9 -  def length_ord(s1: String, s2: String): Boolean =
    1.10 -    s1.length < s2.length || s1.length == s2.length && s1 <= s2
    1.11 -
    1.12 -  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
    1.13 -  {
    1.14 -    require(0 <= start && start <= end && end <= text.length)
    1.15 -
    1.16 -    def this(text: CharSequence) = this(text, 0, text.length)
    1.17 -
    1.18 -    def length: Int = end - start
    1.19 -    def charAt(i: Int): Char = text.charAt(end - i - 1)
    1.20 -
    1.21 -    def subSequence(i: Int, j: Int): CharSequence =
    1.22 -      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
    1.23 -      else throw new IndexOutOfBoundsException
    1.24 -
    1.25 -    override def toString: String =
    1.26 -    {
    1.27 -      val buf = new StringBuilder(length)
    1.28 -      for (i <- 0 until length)
    1.29 -        buf.append(charAt(i))
    1.30 -      buf.toString
    1.31 -    }
    1.32 -  }
    1.33 -
    1.34 -
    1.35    /** word completion **/
    1.36  
    1.37    val word_regex = "[a-zA-Z0-9_']+".r
    1.38 @@ -55,7 +27,7 @@
    1.39  
    1.40      def read(in: CharSequence): Option[String] =
    1.41      {
    1.42 -      val rev_in = new Reverse(in)
    1.43 +      val rev_in = new Library.Reverse(in)
    1.44        parse((rev_symbol | rev_symb | word) ^^ (_.reverse), rev_in) match {
    1.45          case Success(result, _) => Some(result)
    1.46          case _ => None
    1.47 @@ -113,8 +85,8 @@
    1.48  
    1.49    def complete(line: CharSequence): Option[(String, List[String])] =
    1.50    {
    1.51 -    abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
    1.52 -      case abbrevs_lex.Success((rev_a, _), _) =>
    1.53 +    abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
    1.54 +      case abbrevs_lex.Success(rev_a, _) =>
    1.55          val (word, c) = abbrevs_map(rev_a)
    1.56          if (word == c) None
    1.57          else Some(word, List(c))
    1.58 @@ -123,7 +95,7 @@
    1.59            case Some(word) =>
    1.60              words_lex.completions(word).map(words_map(_)).filter(_ != word) match {
    1.61                case Nil => None
    1.62 -              case cs => Some (word, cs.sort(Completion.length_ord _))
    1.63 +              case cs => Some(word, cs.sort(_ < _))
    1.64              }
    1.65            case None => None
    1.66          }

     2.1 --- a/src/Pure/library.scala	Sun Dec 20 15:42:40 2009 +0100
     2.2 +++ b/src/Pure/library.scala	Sun Dec 20 15:44:07 2009 +0100
     2.3 @@ -11,6 +11,31 @@
     2.4  
     2.5  object Library
     2.6  {
     2.7 +  /* reverse CharSequence */
     2.8 +
     2.9 +  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
    2.10 +  {
    2.11 +    require(0 <= start && start <= end && end <= text.length)
    2.12 +
    2.13 +    def this(text: CharSequence) = this(text, 0, text.length)
    2.14 +
    2.15 +    def length: Int = end - start
    2.16 +    def charAt(i: Int): Char = text.charAt(end - i - 1)
    2.17 +
    2.18 +    def subSequence(i: Int, j: Int): CharSequence =
    2.19 +      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
    2.20 +      else throw new IndexOutOfBoundsException
    2.21 +
    2.22 +    override def toString: String =
    2.23 +    {
    2.24 +      val buf = new StringBuilder(length)
    2.25 +      for (i <- 0 until length)
    2.26 +        buf.append(charAt(i))
    2.27 +      buf.toString
    2.28 +    }
    2.29 +  }
    2.30 +
    2.31 +
    2.32    /* timing */
    2.33  
    2.34    def timeit[A](e: => A) =