added spell-checker completion dialog, without counting frequency of items due to empty name;
tuned signature;
--- a/src/Pure/General/completion.scala Sun Apr 13 19:55:16 2014 +0200
+++ b/src/Pure/General/completion.scala Sun Apr 13 21:43:25 2014 +0200
@@ -91,7 +91,8 @@
def + (entry: (String, Int)): History =
{
val (name, freq) = entry
- new History(rep + (name -> (frequency(name) + freq)))
+ if (name == "") this
+ else new History(rep + (name -> (frequency(name) + freq)))
}
def ordering: Ordering[Item] =
--- a/src/Tools/jEdit/src/completion_popup.scala Sun Apr 13 19:55:16 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Sun Apr 13 21:43:25 2014 +0200
@@ -188,6 +188,41 @@
}
+ /* spell-checker completion */
+
+ def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
+ {
+ PIDE.spell_checker.get match {
+ case Some(spell_checker) =>
+ val caret_range = before_caret_range(rendering)
+
+ val result =
+ for {
+ spell_range <- rendering.spell_checker_point(caret_range)
+ text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
+ caret_range0 = caret_range - spell_range.start
+ Text.Info(range0, word) <-
+ Spell_Checker.marked_words(text,
+ info => info.range.overlaps(caret_range0)).headOption
+ } yield Text.Info(range0 + spell_range.start, word)
+
+ result match {
+ case Some(Text.Info(range, original)) =>
+ val words = spell_checker.complete(original)
+ if (words.isEmpty) None
+ else {
+ val descr = "(from dictionary " + quote(spell_checker.toString) + ")"
+ val items = words.map(word =>
+ Completion.Item(range, original, "", List(word, descr), word, 0, false))
+ Some(Completion.Result(range, original, false, items))
+ }
+ case None => None
+ }
+ case None => None
+ }
+ }
+
+
/* completion action: text area */
private def insert(item: Completion.Item)
@@ -318,9 +353,15 @@
}
if (no_completion) false
else {
- val result =
+ val result0 =
Completion.Result.merge(history,
semantic_completion, syntax_completion(history, explicit, opt_rendering))
+ val result =
+ opt_rendering match {
+ case None => result0
+ case Some(rendering) =>
+ Completion.Result.merge(history, result0, spell_checker_completion(rendering))
+ }
result match {
case Some(result) =>
--- a/src/Tools/jEdit/src/rendering.scala Sun Apr 13 19:55:16 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Sun Apr 13 21:43:25 2014 +0200
@@ -292,6 +292,12 @@
def spell_checker_ranges(range: Text.Range): List[Text.Range] =
snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
+ def spell_checker_point(range: Text.Range): Option[Text.Range] =
+ snapshot.select(range, spell_checker_elements, _ =>
+ {
+ case info => Some(snapshot.convert(info.range))
+ }).headOption.map(_.info)
+
/* command status overview */
--- a/src/Tools/jEdit/src/rich_text_area.scala Sun Apr 13 19:55:16 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sun Apr 13 21:43:25 2014 +0200
@@ -322,8 +322,8 @@
spell_checker <- PIDE.spell_checker.get
range0 <- rendering.spell_checker_ranges(line_range)
text <- JEdit_Lib.try_get_text(buffer, range0)
- range <- spell_checker.marked_words(text)
- r <- JEdit_Lib.gfx_range(text_area, range + range0.start)
+ info <- spell_checker.marked_words(text)
+ r <- JEdit_Lib.gfx_range(text_area, info.range + range0.start)
} {
gfx.setColor(rendering.spell_checker_color)
val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2))
--- a/src/Tools/jEdit/src/spell_checker.scala Sun Apr 13 19:55:16 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala Sun Apr 13 21:43:25 2014 +0200
@@ -22,9 +22,9 @@
{
/* marked words within text */
- def marked_words(text: String, mark: String => Boolean): List[Text.Range] =
+ def marked_words(text: String, mark: Text.Info[String] => Boolean): List[Text.Info[String]] =
{
- val result = new mutable.ListBuffer[Text.Range]
+ val result = new mutable.ListBuffer[Text.Info[String]]
var offset = 0
def apostrophe(c: Int): Boolean =
@@ -46,8 +46,10 @@
val start = offset
scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
val stop = offset
- if (stop - start >= 2 && mark(text.substring(start, stop)))
- result += Text.Range(start, stop)
+ if (stop - start >= 2) {
+ val info = Text.Info(Text.Range(start, stop), text.substring(start, stop))
+ if (mark(info)) result += info
+ }
}
result.toList
}
@@ -113,15 +115,15 @@
/* create spell checker */
- def apply(dict: Dictionary): Spell_Checker = new Spell_Checker(dict)
+ def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
}
-class Spell_Checker private(dict: Spell_Checker.Dictionary)
+class Spell_Checker private(dictionary: Spell_Checker.Dictionary)
{
- override def toString: String = dict.toString
+ override def toString: String = dictionary.toString
- private val dictionary =
+ private val dict =
{
val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
val factory_cons = factory_class.getConstructor()
@@ -130,7 +132,7 @@
val add = factory_class.getDeclaredMethod("add", classOf[String])
add.setAccessible(true)
- dict.load_words.foreach(add.invoke(factory, _))
+ dictionary.load_words.foreach(add.invoke(factory, _))
val create = factory_class.getDeclaredMethod("create")
create.setAccessible(true)
@@ -139,35 +141,34 @@
def add(word: String)
{
- val m = dictionary.getClass.getDeclaredMethod("add", classOf[String])
+ val m = dict.getClass.getDeclaredMethod("add", classOf[String])
m.setAccessible(true)
- m.invoke(dictionary, word)
+ m.invoke(dict, word)
}
def contains(word: String): Boolean =
{
- val m = dictionary.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String])
+ val m = dict.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String])
m.setAccessible(true)
- m.invoke(dictionary, word).asInstanceOf[java.lang.Boolean].booleanValue
+ m.invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
}
def check(word: String): Boolean =
contains(word) ||
- Library.is_all_caps(word) && contains(Library.lowercase(word, dict.locale)) ||
+ Library.is_all_caps(word) && contains(Library.lowercase(word, dictionary.locale)) ||
Library.is_capitalized(word) &&
- (contains(Library.lowercase(word, dict.locale)) ||
- contains(Library.uppercase(word, dict.locale)))
+ (contains(Library.lowercase(word, dictionary.locale)) ||
+ contains(Library.uppercase(word, dictionary.locale)))
def complete(word: String): List[String] =
{
- val m = dictionary.getClass.getSuperclass.
- getDeclaredMethod("searchSuggestions", classOf[String])
+ val m = dict.getClass.getSuperclass. getDeclaredMethod("searchSuggestions", classOf[String])
m.setAccessible(true)
- m.invoke(dictionary, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
+ m.invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
}
- def marked_words(text: String): List[Text.Range] =
- Spell_Checker.marked_words(text, w => !check(w))
+ def marked_words(text: String): List[Text.Info[String]] =
+ Spell_Checker.marked_words(text, info => !check(info.info))
}
@@ -183,9 +184,9 @@
val lang = options.string("spell_checker_language")
if (current_spell_checker._1 != lang) {
Spell_Checker.dictionaries.find(_.lang == lang) match {
- case Some(dict) =>
+ case Some(dictionary) =>
val spell_checker =
- Exn.capture { Spell_Checker(dict) } match {
+ Exn.capture { Spell_Checker(dictionary) } match {
case Exn.Res(spell_checker) => Some(spell_checker)
case Exn.Exn(_) => None
}