# HG changeset patch # User wenzelm # Date 1412527444 -7200 # Node ID d4d97b79f1fbbdef760bd0b99e0f449840e7e085 # Parent d0ee64efd6241d1a9119b75afff5f8698c67ff39 clarified modules; diff -r d0ee64efd624 -r d4d97b79f1fb src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Sun Oct 05 18:30:43 2014 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Sun Oct 05 18:44:04 2014 +0200 @@ -179,26 +179,6 @@ } - /* spell-checker completion */ - - def spell_checker_completion( - explicit: Boolean, - rendering: Rendering): Option[Completion.Result] = - { - for { - spell_checker <- PIDE.spell_checker.get - if explicit - range = JEdit_Lib.before_caret_range(text_area, rendering) - word <- Spell_Checker.current_word(text_area, rendering, range) - words = spell_checker.complete(word.info) - if !words.isEmpty - descr = "(from dictionary " + quote(spell_checker.toString) + ")" - items = - words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false)) - } yield Completion.Result(word.range, word.info, false, items) - } - - /* path completion */ def path_completion(rendering: Rendering): Option[Completion.Result] = @@ -399,7 +379,8 @@ case Some(rendering) => Completion.Result.merge(history, result0, Completion.Result.merge(history, - spell_checker_completion(explicit, rendering), path_completion(rendering))) + Spell_Checker.completion(text_area, explicit, rendering), + path_completion(rendering))) } } result match { diff -r d0ee64efd624 -r d4d97b79f1fb src/Tools/jEdit/src/context_menu.scala --- a/src/Tools/jEdit/src/context_menu.scala Sun Oct 05 18:30:43 2014 +0200 +++ b/src/Tools/jEdit/src/context_menu.scala Sun Oct 05 18:44:04 2014 +0200 @@ -14,62 +14,12 @@ import javax.swing.JMenuItem -import org.gjt.sp.jedit.menu.EnhancedMenuItem import org.gjt.sp.jedit.gui.DynamicContextMenuService -import org.gjt.sp.jedit.{jEdit, Buffer} import org.gjt.sp.jedit.textarea.JEditTextArea class Context_Menu extends DynamicContextMenuService { - /* spell checker menu */ - - private def spell_checker_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = - { - val result = - for { - spell_checker <- PIDE.spell_checker.get - doc_view <- PIDE.document_view(text_area) - rendering = doc_view.get_rendering() - range = JEdit_Lib.point_range(text_area.getBuffer, offset) - Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range) - } yield (spell_checker, word) - - result match { - case Some((spell_checker, word)) => - - val context = jEdit.getActionContext() - def item(name: String): JMenuItem = - new EnhancedMenuItem(context.getAction(name).getLabel, name, context) - - val complete_items = - if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word")) - else Nil - - val update_items = - if (spell_checker.check(word)) - List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently")) - else - List(item("isabelle.include-word"), item("isabelle.include-word-permanently")) - - val reset_items = - spell_checker.reset_enabled() match { - case 0 => Nil - case n => - val name = "isabelle.reset-words" - val label = context.getAction(name).getLabel - List(new EnhancedMenuItem(label + " (" + n + ")", name, context)) - } - - complete_items ::: update_items ::: reset_items - - case None => Nil - } - } - - - /* menu service */ - def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] = { PIDE.dismissed_popups(text_area.getView) @@ -77,7 +27,7 @@ val items1 = if (evt != null && evt.getSource == text_area.getPainter) { val offset = text_area.xyToOffset(evt.getX, evt.getY) - if (offset >= 0) spell_checker_menu(text_area, offset) + if (offset >= 0) Spell_Checker.context_menu(text_area, offset) else Nil } else Nil diff -r d0ee64efd624 -r d4d97b79f1fb src/Tools/jEdit/src/spell_checker.scala --- a/src/Tools/jEdit/src/spell_checker.scala Sun Oct 05 18:30:43 2014 +0200 +++ b/src/Tools/jEdit/src/spell_checker.scala Sun Oct 05 18:44:04 2014 +0200 @@ -12,17 +12,21 @@ import java.lang.Class +import javax.swing.JMenuItem + import scala.collection.mutable import scala.swing.ComboBox import scala.annotation.tailrec import scala.collection.immutable.SortedMap -import org.gjt.sp.jedit.textarea.TextArea +import org.gjt.sp.jedit.menu.EnhancedMenuItem +import org.gjt.sp.jedit.{jEdit, Buffer} +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} object Spell_Checker { - /* words within text */ + /** words within text **/ def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean) : List[Text.Info[String]] = @@ -68,7 +72,77 @@ } - /* dictionary declarations */ + + /** completion **/ + + def completion(text_area: TextArea, explicit: Boolean, rendering: Rendering) + : Option[Completion.Result] = + { + for { + spell_checker <- PIDE.spell_checker.get + if explicit + range = JEdit_Lib.before_caret_range(text_area, rendering) + word <- current_word(text_area, rendering, range) + words = spell_checker.complete(word.info) + if !words.isEmpty + descr = "(from dictionary " + quote(spell_checker.toString) + ")" + items = + words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false)) + } yield Completion.Result(word.range, word.info, false, items) + } + + + + /** context menu **/ + + def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = + { + val result = + for { + spell_checker <- PIDE.spell_checker.get + doc_view <- PIDE.document_view(text_area) + rendering = doc_view.get_rendering() + range = JEdit_Lib.point_range(text_area.getBuffer, offset) + Text.Info(_, word) <- current_word(text_area, rendering, range) + } yield (spell_checker, word) + + result match { + case Some((spell_checker, word)) => + + val context = jEdit.getActionContext() + def item(name: String): JMenuItem = + new EnhancedMenuItem(context.getAction(name).getLabel, name, context) + + val complete_items = + if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word")) + else Nil + + val update_items = + if (spell_checker.check(word)) + List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently")) + else + List(item("isabelle.include-word"), item("isabelle.include-word-permanently")) + + val reset_items = + spell_checker.reset_enabled() match { + case 0 => Nil + case n => + val name = "isabelle.reset-words" + val label = context.getAction(name).getLabel + List(new EnhancedMenuItem(label + " (" + n + ")", name, context)) + } + + complete_items ::: update_items ::: reset_items + + case None => Nil + } + } + + + + /** dictionary **/ + + /* declarations */ class Dictionary private[Spell_Checker](val path: Path) {