# HG changeset patch # User haftmann # Date 1245783959 -7200 # Node ID 496c86f5f9e93870af61d284fe90b9897585cf69 # Parent 4751b2a2c5c873558fa0a7838768d699f0b15d32# Parent eb174cfdef1a4e91162247a9ea7d96443ccaf5f2 merged diff -r 4751b2a2c5c8 -r 496c86f5f9e9 src/Pure/General/scan.scala --- 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 - } - } - } diff -r 4751b2a2c5c8 -r 496c86f5f9e9 src/Pure/IsaMakefile --- 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 diff -r 4751b2a2c5c8 -r 496c86f5f9e9 src/Pure/Thy/completion.scala --- /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 + } + } + } +}