# HG changeset patch
# User wenzelm
# Date 1397552748 -7200
# Node ID a0e844c6e1edca98a400937a4664e453089262df
# Parent  9ccbac38bcad1159a59b8e7727243df5c27b55da
common context menu for Isabelle/jEdit;

diff -r 9ccbac38bcad -r a0e844c6e1ed src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Apr 15 10:44:38 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Apr 15 11:05:48 2014 +0200
@@ -10,6 +10,7 @@
 declare -a SOURCES=(
   "src/active.scala"
   "src/completion_popup.scala"
+  "src/context_menu.scala"
   "src/dockable.scala"
   "src/document_model.scala"
   "src/document_view.scala"
diff -r 9ccbac38bcad -r a0e844c6e1ed src/Tools/jEdit/src/context_menu.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/context_menu.scala	Tue Apr 15 11:05:48 2014 +0200
@@ -0,0 +1,74 @@
+/*  Title:      Tools/jEdit/src/context_menu.scala
+    Author:     Makarius
+
+Common context menu for Isabelle/jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import java.awt.event.MouseEvent
+import javax.swing.JMenuItem
+
+import org.gjt.sp.jedit.menu.EnhancedMenuItem
+import org.gjt.sp.jedit.gui.DynamicContextMenuService
+import org.gjt.sp.jedit.jEdit
+import org.gjt.sp.jedit.textarea.JEditTextArea
+
+
+class Context_Menu extends DynamicContextMenuService
+{
+  /* spell checker menu */
+
+  private def action_item(name: String): JMenuItem =
+  {
+    val context = jEdit.getActionContext()
+    new EnhancedMenuItem(context.getAction(name).getLabel, name, context)
+  }
+
+  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.check(word)
+
+    result match {
+      case Some(false) =>
+        List(
+          action_item("isabelle.include-word"),
+          action_item("isabelle.include-word-permanently"),
+          action_item("isabelle.reset-words"))
+      case Some(true) =>
+        List(
+          action_item("isabelle.exclude-word"),
+          action_item("isabelle.exclude-word-permanently"),
+          action_item("isabelle.reset-words"))
+      case None => Nil
+    }
+  }
+
+
+  /* menu service */
+
+  def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
+  {
+    if (evt != null && evt.getSource == text_area.getPainter) {
+      val offset = text_area.xyToOffset(evt.getX, evt.getY)
+      if (offset >= 0) {
+        val items = spell_checker_menu(text_area, offset)
+        if (items.isEmpty) null else items.toArray
+      }
+      else null
+    }
+    else null
+  }
+}
+
diff -r 9ccbac38bcad -r a0e844c6e1ed src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml	Tue Apr 15 10:44:38 2014 +0200
+++ b/src/Tools/jEdit/src/services.xml	Tue Apr 15 11:05:48 2014 +0200
@@ -3,7 +3,7 @@
 
 <SERVICES>
   <SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
-    new isabelle.jedit.Spell_Checker_Menu();
+    new isabelle.jedit.Context_Menu();
   </SERVICE>
   <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
     new isabelle.jedit.Isabelle_Encoding();
diff -r 9ccbac38bcad -r a0e844c6e1ed src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 15 10:44:38 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 15 11:05:48 2014 +0200
@@ -11,18 +11,13 @@
 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.jEdit
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
-import org.gjt.sp.jedit.menu.EnhancedMenuItem
-import org.gjt.sp.jedit.gui.DynamicContextMenuService
+import org.gjt.sp.jedit.textarea.TextArea
 
 
 object Spell_Checker
@@ -295,43 +290,3 @@
   }
 }
 
-
-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"),
-              item("isabelle.reset-words"))
-          else
-            Array(
-              item("isabelle.include-word"),
-              item("isabelle.include-word-permanently"),
-              item("isabelle.reset-words"))
-
-        case None => null
-      }
-    }
-    else null
-  }
-}