# HG changeset patch
# User wenzelm
# Date 1397509990 -7200
# Node ID 86148ca3c4fd0710c265d6844d2f9b8b0bfebc94
# Parent  cdd609ea595dfd794399495fba8845d97db82bb8
added context menu for spell checker actions;

diff -r cdd609ea595d -r 86148ca3c4fd src/Tools/jEdit/src/completion_popup.scala
--- 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
diff -r cdd609ea595d -r 86148ca3c4fd src/Tools/jEdit/src/isabelle.scala
--- 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())
diff -r cdd609ea595d -r 86148ca3c4fd src/Tools/jEdit/src/services.xml
--- 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>
diff -r cdd609ea595d -r 86148ca3c4fd src/Tools/jEdit/src/spell_checker.scala
--- 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
+  }
+}