added context menu for spell checker actions;
authorwenzelm
Mon Apr 14 23:13:10 2014 +0200 (2014-04-14 ago)
changeset 5657686148ca3c4fd
parent 56575 cdd609ea595d
child 56577 58d7960058f5
added context menu for spell checker actions;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/services.xml
src/Tools/jEdit/src/spell_checker.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 14 22:51:23 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 14 23:13:10 2014 +0200
     1.3 @@ -183,7 +183,8 @@
     1.4      def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
     1.5        PIDE.spell_checker.get match {
     1.6          case Some(spell_checker) =>
     1.7 -          Spell_Checker.current_word(text_area, rendering) match {
     1.8 +          val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
     1.9 +          Spell_Checker.current_word(text_area, rendering, caret_range) match {
    1.10              case Some(Text.Info(range, original)) =>
    1.11                val words = spell_checker.complete(original)
    1.12                if (words.isEmpty) None
     2.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Apr 14 22:51:23 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Apr 14 23:13:10 2014 +0200
     2.3 @@ -298,7 +298,9 @@
     2.4      for {
     2.5        spell_checker <- PIDE.spell_checker.get
     2.6        doc_view <- PIDE.document_view(text_area)
     2.7 -      Text.Info(_, word) <- Spell_Checker.current_word(text_area, doc_view.get_rendering())
     2.8 +      rendering = doc_view.get_rendering()
     2.9 +      range = JEdit_Lib.before_caret_range(text_area, rendering)
    2.10 +      Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
    2.11      } {
    2.12        spell_checker.update(word, include, permanent)
    2.13        JEdit_Lib.jedit_views().foreach(_.repaint())
     3.1 --- a/src/Tools/jEdit/src/services.xml	Mon Apr 14 22:51:23 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/services.xml	Mon Apr 14 23:13:10 2014 +0200
     3.3 @@ -2,25 +2,28 @@
     3.4  <!DOCTYPE SERVICES SYSTEM "services.dtd">
     3.5  
     3.6  <SERVICES>
     3.7 -	<SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
     3.8 -		new isabelle.jedit.Isabelle_Encoding();
     3.9 -	</SERVICE>
    3.10 -	<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
    3.11 -		new isabelle.jedit.Isabelle_Sidekick_Default();
    3.12 -	</SERVICE>
    3.13 -	<SERVICE NAME="isabelle-markup" CLASS="sidekick.SideKickParser">
    3.14 -		new isabelle.jedit.Isabelle_Sidekick_Markup();
    3.15 -	</SERVICE>
    3.16 -	<SERVICE NAME="isabelle-news" CLASS="sidekick.SideKickParser">
    3.17 -		new isabelle.jedit.Isabelle_Sidekick_News();
    3.18 -	</SERVICE>
    3.19 -	<SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
    3.20 -		new isabelle.jedit.Isabelle_Sidekick_Options();
    3.21 -	</SERVICE>
    3.22 -	<SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
    3.23 -		new isabelle.jedit.Isabelle_Sidekick_Root();
    3.24 -	</SERVICE>
    3.25 - 	<SERVICE CLASS="console.Shell" NAME="Scala">
    3.26 -		new isabelle.jedit.Scala_Console();
    3.27 -	</SERVICE>
    3.28 +  <SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
    3.29 +    new isabelle.jedit.Spell_Checker_Menu();
    3.30 +  </SERVICE>
    3.31 +  <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
    3.32 +    new isabelle.jedit.Isabelle_Encoding();
    3.33 +  </SERVICE>
    3.34 +  <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
    3.35 +    new isabelle.jedit.Isabelle_Sidekick_Default();
    3.36 +  </SERVICE>
    3.37 +  <SERVICE NAME="isabelle-markup" CLASS="sidekick.SideKickParser">
    3.38 +    new isabelle.jedit.Isabelle_Sidekick_Markup();
    3.39 +  </SERVICE>
    3.40 +  <SERVICE NAME="isabelle-news" CLASS="sidekick.SideKickParser">
    3.41 +    new isabelle.jedit.Isabelle_Sidekick_News();
    3.42 +  </SERVICE>
    3.43 +  <SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
    3.44 +    new isabelle.jedit.Isabelle_Sidekick_Options();
    3.45 +  </SERVICE>
    3.46 +  <SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
    3.47 +    new isabelle.jedit.Isabelle_Sidekick_Root();
    3.48 +  </SERVICE>
    3.49 +  <SERVICE CLASS="console.Shell" NAME="Scala">
    3.50 +    new isabelle.jedit.Scala_Console();
    3.51 +  </SERVICE>
    3.52  </SERVICES>
     4.1 --- a/src/Tools/jEdit/src/spell_checker.scala	Mon Apr 14 22:51:23 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/spell_checker.scala	Mon Apr 14 23:13:10 2014 +0200
     4.3 @@ -11,13 +11,18 @@
     4.4  import isabelle._
     4.5  
     4.6  import java.lang.Class
     4.7 +import java.awt.event.MouseEvent
     4.8 +import javax.swing.JMenuItem
     4.9  
    4.10  import scala.collection.mutable
    4.11  import scala.swing.ComboBox
    4.12  import scala.annotation.tailrec
    4.13  import scala.collection.immutable.SortedMap
    4.14  
    4.15 -import org.gjt.sp.jedit.textarea.TextArea
    4.16 +import org.gjt.sp.jedit.jEdit
    4.17 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    4.18 +import org.gjt.sp.jedit.menu.EnhancedMenuItem;
    4.19 +import org.gjt.sp.jedit.gui.DynamicContextMenuService;
    4.20  
    4.21  
    4.22  object Spell_Checker
    4.23 @@ -57,13 +62,13 @@
    4.24      result.toList
    4.25    }
    4.26  
    4.27 -  def current_word(text_area: TextArea, rendering: Rendering): Option[Text.Info[String]] =
    4.28 +  def current_word(text_area: TextArea, rendering: Rendering, range: Text.Range)
    4.29 +    : Option[Text.Info[String]] =
    4.30    {
    4.31 -    val caret = JEdit_Lib.before_caret_range(text_area, rendering)
    4.32      for {
    4.33 -      spell_range <- rendering.spell_checker_point(caret)
    4.34 +      spell_range <- rendering.spell_checker_point(range)
    4.35        text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
    4.36 -      info <- marked_words(spell_range.start, text, info => info.range.overlaps(caret)).headOption
    4.37 +      info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
    4.38      } yield info
    4.39    }
    4.40  
    4.41 @@ -292,3 +297,38 @@
    4.42      else current_spell_checker = no_spell_checker
    4.43    }
    4.44  }
    4.45 +
    4.46 +
    4.47 +class Spell_Checker_Menu extends DynamicContextMenuService
    4.48 +{
    4.49 +  def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
    4.50 +  {
    4.51 +    if (evt != null && evt.getSource == text_area.getPainter) {
    4.52 +      val result =
    4.53 +        for {
    4.54 +          spell_checker <- PIDE.spell_checker.get
    4.55 +          doc_view <- PIDE.document_view(text_area)
    4.56 +          rendering = doc_view.get_rendering()
    4.57 +          offset = text_area.xyToOffset(evt.getX, evt.getY)
    4.58 +          if offset >= 0
    4.59 +          range = JEdit_Lib.point_range(text_area.getBuffer, offset)
    4.60 +          Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
    4.61 +        } yield spell_checker.check(word)
    4.62 +
    4.63 +      result match {
    4.64 +        case Some(known_word) =>
    4.65 +          val context = jEdit.getActionContext()
    4.66 +          def item(action: String) =
    4.67 +            new EnhancedMenuItem(context.getAction(action).getLabel, action, context)
    4.68 +
    4.69 +          if (known_word)
    4.70 +            Array(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
    4.71 +          else
    4.72 +            Array(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
    4.73 +
    4.74 +        case None => null
    4.75 +      }
    4.76 +    }
    4.77 +    else null
    4.78 +  }
    4.79 +}