--- a/src/Tools/jEdit/src/completion_popup.scala Mon Apr 14 22:51:23 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Apr 14 23:13:10 2014 +0200
@@ -183,7 +183,8 @@
def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
PIDE.spell_checker.get match {
case Some(spell_checker) =>
- Spell_Checker.current_word(text_area, rendering) match {
+ val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
+ Spell_Checker.current_word(text_area, rendering, caret_range) match {
case Some(Text.Info(range, original)) =>
val words = spell_checker.complete(original)
if (words.isEmpty) None
--- a/src/Tools/jEdit/src/isabelle.scala Mon Apr 14 22:51:23 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Apr 14 23:13:10 2014 +0200
@@ -298,7 +298,9 @@
for {
spell_checker <- PIDE.spell_checker.get
doc_view <- PIDE.document_view(text_area)
- Text.Info(_, word) <- Spell_Checker.current_word(text_area, doc_view.get_rendering())
+ rendering = doc_view.get_rendering()
+ range = JEdit_Lib.before_caret_range(text_area, rendering)
+ Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
} {
spell_checker.update(word, include, permanent)
JEdit_Lib.jedit_views().foreach(_.repaint())
--- a/src/Tools/jEdit/src/services.xml Mon Apr 14 22:51:23 2014 +0200
+++ b/src/Tools/jEdit/src/services.xml Mon Apr 14 23:13:10 2014 +0200
@@ -2,25 +2,28 @@
<!DOCTYPE SERVICES SYSTEM "services.dtd">
<SERVICES>
- <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
- new isabelle.jedit.Isabelle_Encoding();
- </SERVICE>
- <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_Default();
- </SERVICE>
- <SERVICE NAME="isabelle-markup" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_Markup();
- </SERVICE>
- <SERVICE NAME="isabelle-news" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_News();
- </SERVICE>
- <SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_Options();
- </SERVICE>
- <SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_Root();
- </SERVICE>
- <SERVICE CLASS="console.Shell" NAME="Scala">
- new isabelle.jedit.Scala_Console();
- </SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
+ new isabelle.jedit.Spell_Checker_Menu();
+ </SERVICE>
+ <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
+ new isabelle.jedit.Isabelle_Encoding();
+ </SERVICE>
+ <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_Default();
+ </SERVICE>
+ <SERVICE NAME="isabelle-markup" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_Markup();
+ </SERVICE>
+ <SERVICE NAME="isabelle-news" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_News();
+ </SERVICE>
+ <SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_Options();
+ </SERVICE>
+ <SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_Root();
+ </SERVICE>
+ <SERVICE CLASS="console.Shell" NAME="Scala">
+ new isabelle.jedit.Scala_Console();
+ </SERVICE>
</SERVICES>
--- a/src/Tools/jEdit/src/spell_checker.scala Mon Apr 14 22:51:23 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala Mon Apr 14 23:13:10 2014 +0200
@@ -11,13 +11,18 @@
import isabelle._
import java.lang.Class
+import java.awt.event.MouseEvent
+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.jEdit
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+import org.gjt.sp.jedit.menu.EnhancedMenuItem;
+import org.gjt.sp.jedit.gui.DynamicContextMenuService;
object Spell_Checker
@@ -57,13 +62,13 @@
result.toList
}
- def current_word(text_area: TextArea, rendering: Rendering): Option[Text.Info[String]] =
+ def current_word(text_area: TextArea, rendering: Rendering, range: Text.Range)
+ : Option[Text.Info[String]] =
{
- val caret = JEdit_Lib.before_caret_range(text_area, rendering)
for {
- spell_range <- rendering.spell_checker_point(caret)
+ spell_range <- rendering.spell_checker_point(range)
text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
- info <- marked_words(spell_range.start, text, info => info.range.overlaps(caret)).headOption
+ info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
} yield info
}
@@ -292,3 +297,38 @@
else current_spell_checker = no_spell_checker
}
}
+
+
+class Spell_Checker_Menu extends DynamicContextMenuService
+{
+ def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
+ {
+ if (evt != null && evt.getSource == text_area.getPainter) {
+ val result =
+ for {
+ spell_checker <- PIDE.spell_checker.get
+ doc_view <- PIDE.document_view(text_area)
+ rendering = doc_view.get_rendering()
+ offset = text_area.xyToOffset(evt.getX, evt.getY)
+ if offset >= 0
+ range = JEdit_Lib.point_range(text_area.getBuffer, offset)
+ Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
+ } yield spell_checker.check(word)
+
+ result match {
+ case Some(known_word) =>
+ val context = jEdit.getActionContext()
+ def item(action: String) =
+ new EnhancedMenuItem(context.getAction(action).getLabel, action, context)
+
+ if (known_word)
+ Array(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
+ else
+ Array(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
+
+ case None => null
+ }
+ }
+ else null
+ }
+}