--- a/src/Pure/General/scan.scala Tue Jun 23 21:03:31 2009 +0200
+++ b/src/Pure/General/scan.scala Tue Jun 23 21:05:59 2009 +0200
@@ -19,19 +19,16 @@
private case class Tree(val branches: Map[Char, (String, Tree)])
private val empty_tree = Tree(Map())
- 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)
+ def apply(elems: String*): Lexicon = empty ++ elems
}
- class Lexicon extends scala.collection.immutable.Set[String] with RegexParsers
+ class Lexicon extends scala.collection.Set[String] with RegexParsers
{
/* representation */
import Lexicon.Tree
- val main_tree: Tree = Lexicon.empty_tree
+ protected val main_tree: Tree = Lexicon.empty_tree
/* auxiliary operations */
@@ -57,13 +54,11 @@
}
def completions(str: CharSequence): List[String] =
- {
- (lookup(str) match {
+ 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 */
@@ -75,34 +70,37 @@
def size: Int = content(main_tree, Nil).length
def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
- def contains(str: String): Boolean =
- lookup(str) match {
+ def contains(elem: String): Boolean =
+ lookup(elem) match {
case Some((tip, _)) => tip
case _ => false
}
- def +(str: String): Lexicon =
- {
- val len = str.length
- def extend(tree: Tree, i: Int): Tree =
- {
- if (i < len) {
- val c = str.charAt(i)
- val end = (i + 1 == len)
- tree.branches.get(c) match {
- case Some((s, tr)) =>
- Tree(tree.branches + (c -> (if (end) str else s, extend(tr, i + 1))))
- case None =>
- Tree(tree.branches + (c -> (if (end) str else "", extend(Lexicon.empty_tree, i + 1))))
- }
- } else tree
+ def + (elem: String): Lexicon =
+ if (contains(elem)) this
+ else {
+ val len = elem.length
+ def extend(tree: Tree, i: Int): Tree =
+ if (i < len) {
+ val c = elem.charAt(i)
+ val end = (i + 1 == len)
+ tree.branches.get(c) match {
+ case Some((s, tr)) =>
+ Tree(tree.branches +
+ (c -> (if (end) elem else s, extend(tr, i + 1))))
+ case None =>
+ Tree(tree.branches +
+ (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
+ }
+ } else tree
+ val old = this
+ new Lexicon { override val main_tree = extend(old.main_tree, 0) }
}
- if (contains(str)) this
- else Lexicon.make(extend(main_tree, 0))
- }
- def empty[A]: Set[A] = error("Undefined")
- def -(str: String): Lexicon = error("Undefined")
+ def + (elem1: String, elem2: String, elems: String*): Lexicon =
+ this + elem1 + elem2 ++ elems
+ def ++ (elems: Iterable[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
+ def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
/* RegexParsers methods */
@@ -132,31 +130,5 @@
}.named("keyword")
}
-
-
- /** 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 StringBuffer(length)
- for (i <- 0 until length)
- buf.append(charAt(i))
- buf.toString
- }
- }
-
}
--- a/src/Pure/IsaMakefile Tue Jun 23 21:03:31 2009 +0200
+++ b/src/Pure/IsaMakefile Tue Jun 23 21:05:59 2009 +0200
@@ -122,8 +122,8 @@
General/symbol.scala General/xml.scala General/yxml.scala \
Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala \
System/cygwin.scala System/isabelle_process.scala \
- System/isabelle_system.scala Thy/thy_header.scala \
- Tools/isabelle_syntax.scala
+ System/isabelle_system.scala Thy/completion.scala \
+ Thy/thy_header.scala Tools/isabelle_syntax.scala
SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/completion.scala Tue Jun 23 21:05:59 2009 +0200
@@ -0,0 +1,131 @@
+/* Title: Pure/Thy/completion.scala
+ Author: Makarius
+
+Completion of symbols and keywords.
+*/
+
+package isabelle
+
+import scala.util.matching.Regex
+import scala.util.parsing.combinator.RegexParsers
+
+
+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 StringBuffer(length)
+ for (i <- 0 until length)
+ buf.append(charAt(i))
+ buf.toString
+ }
+ }
+
+
+ /** word completion **/
+
+ val word_regex = "[a-zA-Z0-9_']+".r
+ def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
+
+ object Parse extends RegexParsers
+ {
+ override val whiteSpace = "".r
+
+ def rev_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
+ def rev_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
+ def word: Parser[String] = "[a-zA-Z0-9_']{3,}".r
+
+ def read(in: CharSequence): Option[String] =
+ {
+ val rev_in = new Reverse(in)
+ parse((rev_symbol | rev_symb | word) ^^ (_.reverse), rev_in) match {
+ case Success(result, _) => Some(result)
+ case _ => None
+ }
+ }
+ }
+}
+
+class Completion
+{
+ /* representation */
+
+ val words_lex = Scan.Lexicon()
+ val words_map = Map[String, String]()
+
+ val abbrevs_lex = Scan.Lexicon()
+ val abbrevs_map = Map[String, (String, String)]()
+
+
+ /* adding stuff */
+
+ def + (keyword: String): Completion =
+ {
+ val old = this
+ new Completion {
+ override val words_lex = old.words_lex + keyword
+ override val words_map = old.words_map + (keyword -> keyword)
+ override val abbrevs_lex = old.abbrevs_lex
+ override val abbrevs_map = old.abbrevs_map
+ }
+ }
+
+ def + (symbols: Symbol.Interpretation): Completion =
+ {
+ val words =
+ (for ((x, _) <- symbols.names) yield (x, x)).toList :::
+ (for ((x, y) <- symbols.names) yield (y, x)).toList :::
+ (for ((x, y) <- symbols.abbrevs if Completion.is_word(y)) yield (y, x)).toList
+
+ val abbrs =
+ (for ((x, y) <- symbols.abbrevs if !Completion.is_word(y))
+ yield (y.reverse.toString, (y, x))).toList
+
+ val old = this
+ new Completion {
+ override val words_lex = old.words_lex ++ words.map(_._1)
+ override val words_map = old.words_map ++ words
+ override val abbrevs_lex = old.abbrevs_lex ++ abbrs.map(_._1)
+ override val abbrevs_map = old.abbrevs_map ++ abbrs
+ }
+ }
+
+
+ /* complete */
+
+ 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, _) =>
+ val (word, c) = abbrevs_map(rev_a)
+ Some(word, List(c))
+ case _ =>
+ Completion.Parse.read(line) match {
+ case Some(word) =>
+ words_lex.completions(word) match {
+ case Nil => None
+ case cs => Some(word, cs.map(words_map(_)).sort(Completion.length_ord _))
+ }
+ case None => None
+ }
+ }
+ }
+}