# HG changeset patch # User wenzelm # Date 1261320247 -3600 # Node ID 297b2149077d06878ec1f9c9e0960f03c830823c # Parent 31be1235d0fbaeb67a2911b09ce92165bfdcd1a6 simiplified result of keyword parser (again); sort completions by plain string order; moved Reverse to library.scala; diff -r 31be1235d0fb -r 297b2149077d src/Pure/Thy/completion.scala --- a/src/Pure/Thy/completion.scala Sun Dec 20 15:42:40 2009 +0100 +++ b/src/Pure/Thy/completion.scala Sun Dec 20 15:44:07 2009 +0100 @@ -12,34 +12,6 @@ private object Completion { - /** String/CharSequence utilities */ - - def length_ord(s1: String, s2: String): Boolean = - s1.length < s2.length || s1.length == s2.length && s1 <= s2 - - class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence - { - require(0 <= start && start <= end && end <= text.length) - - def this(text: CharSequence) = this(text, 0, text.length) - - def length: Int = end - start - def charAt(i: Int): Char = text.charAt(end - i - 1) - - def subSequence(i: Int, j: Int): CharSequence = - if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i) - else throw new IndexOutOfBoundsException - - override def toString: String = - { - val buf = new StringBuilder(length) - for (i <- 0 until length) - buf.append(charAt(i)) - buf.toString - } - } - - /** word completion **/ val word_regex = "[a-zA-Z0-9_']+".r @@ -55,7 +27,7 @@ def read(in: CharSequence): Option[String] = { - val rev_in = new Reverse(in) + val rev_in = new Library.Reverse(in) parse((rev_symbol | rev_symb | word) ^^ (_.reverse), rev_in) match { case Success(result, _) => Some(result) case _ => None @@ -113,8 +85,8 @@ def complete(line: CharSequence): Option[(String, List[String])] = { - abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match { - case abbrevs_lex.Success((rev_a, _), _) => + abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match { + case abbrevs_lex.Success(rev_a, _) => val (word, c) = abbrevs_map(rev_a) if (word == c) None else Some(word, List(c)) @@ -123,7 +95,7 @@ case Some(word) => words_lex.completions(word).map(words_map(_)).filter(_ != word) match { case Nil => None - case cs => Some (word, cs.sort(Completion.length_ord _)) + case cs => Some(word, cs.sort(_ < _)) } case None => None } diff -r 31be1235d0fb -r 297b2149077d src/Pure/library.scala --- a/src/Pure/library.scala Sun Dec 20 15:42:40 2009 +0100 +++ b/src/Pure/library.scala Sun Dec 20 15:44:07 2009 +0100 @@ -11,6 +11,31 @@ object Library { + /* reverse CharSequence */ + + class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence + { + require(0 <= start && start <= end && end <= text.length) + + def this(text: CharSequence) = this(text, 0, text.length) + + def length: Int = end - start + def charAt(i: Int): Char = text.charAt(end - i - 1) + + def subSequence(i: Int, j: Int): CharSequence = + if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i) + else throw new IndexOutOfBoundsException + + override def toString: String = + { + val buf = new StringBuilder(length) + for (i <- 0 until length) + buf.append(charAt(i)) + buf.toString + } + } + + /* timing */ def timeit[A](e: => A) =