added spell-checker completion dialog, without counting frequency of items due to empty name;
authorwenzelm
Sun, 13 Apr 2014 21:43:25 +0200
changeset 56564 94c55cc73747
parent 56563 9ac666f343d4
child 56565 927dff80d0df
added spell-checker completion dialog, without counting frequency of items due to empty name; tuned signature;
src/Pure/General/completion.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/spell_checker.scala
--- 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
               }