# HG changeset patch
# User wenzelm
# Date 1397505101 -7200
# Node ID 2b38472a469543379bb83e93ae29b1ace52d12ac
# Parent  0f9d2e13187e9c4ae37c29c3e33f93879b0cb8d2
some actions to maintain spell-checker dictionary;

diff -r 0f9d2e13187e -r 2b38472a4695 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Mon Apr 14 20:36:50 2014 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Mon Apr 14 21:51:41 2014 +0200
@@ -92,4 +92,29 @@
 	    isabelle.jedit.Isabelle.input_bsup(textArea);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.include-word">
+	  <CODE>
+	    isabelle.jedit.Isabelle.update_dictionary(textArea, true, false);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.include-word-permanently">
+	  <CODE>
+	    isabelle.jedit.Isabelle.update_dictionary(textArea, true, true);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.exclude-word">
+	  <CODE>
+	    isabelle.jedit.Isabelle.update_dictionary(textArea, false, false);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.exclude-word-permanently">
+	  <CODE>
+	    isabelle.jedit.Isabelle.update_dictionary(textArea, false, true);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.reset-words">
+	  <CODE>
+	    isabelle.jedit.Isabelle.reset_dictionary();
+	  </CODE>
+	</ACTION>
 </ACTIONS>
diff -r 0f9d2e13187e -r 2b38472a4695 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 14 20:36:50 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 14 21:51:41 2014 +0200
@@ -119,16 +119,6 @@
       }
 
 
-    /* caret */
-
-    def before_caret_range(rendering: Rendering): Text.Range =
-    {
-      val snapshot = rendering.snapshot
-      val former_caret = snapshot.revert(text_area.getCaretPosition)
-      snapshot.convert(Text.Range(former_caret - 1, former_caret))
-    }
-
-
     /* rendering */
 
     def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
@@ -138,7 +128,7 @@
         case None =>
           val buffer = text_area.getBuffer
           if (line_range.contains(text_area.getCaretPosition)) {
-            before_caret_range(rendering).try_restrict(line_range) match {
+            JEdit_Lib.before_caret_range(text_area, rendering).try_restrict(line_range) match {
               case Some(range) if !range.is_singularity =>
                 rendering.semantic_completion(range) match {
                   case Some(Text.Info(_, Completion.No_Completion)) => None
@@ -176,7 +166,7 @@
           val context =
             (opt_rendering match {
               case Some(rendering) =>
-                rendering.language_context(before_caret_range(rendering))
+                rendering.language_context(JEdit_Lib.before_caret_range(text_area, rendering))
               case None => None
             }) getOrElse syntax.language_context
 
@@ -191,21 +181,9 @@
     /* spell-checker completion */
 
     def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
-    {
       PIDE.spell_checker.get match {
         case Some(spell_checker) =>
-          val caret_range = before_caret_range(rendering)
-
-          val result =
-            for {
-              spell_range <- rendering.spell_checker_point(caret_range)
-              text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
-              info <-
-                Spell_Checker.marked_words(spell_range.start, text,
-                  info => info.range.overlaps(caret_range)).headOption
-            } yield info
-
-          result match {
+          Spell_Checker.current_word(text_area, rendering) match {
             case Some(Text.Info(range, original)) =>
               val words = spell_checker.complete(original)
               if (words.isEmpty) None
@@ -219,7 +197,6 @@
           }
         case None => None
       }
-    }
 
 
     /* completion action: text area */
@@ -332,7 +309,8 @@
             case Some(doc_view) =>
               val rendering = doc_view.get_rendering()
               val (no_completion, result) =
-                rendering.semantic_completion(before_caret_range(rendering)) match {
+                rendering.semantic_completion(JEdit_Lib.before_caret_range(text_area, rendering))
+                match {
                   case Some(Text.Info(_, Completion.No_Completion)) =>
                     (true, None)
                   case Some(Text.Info(range, names: Completion.Names)) =>
diff -r 0f9d2e13187e -r 2b38472a4695 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Apr 14 20:36:50 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Apr 14 21:51:41 2014 +0200
@@ -289,5 +289,19 @@
 
   def input_bsup(text_area: JEditTextArea)
   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
+
+
+  /* spell-checker dictionary */
+
+  def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
+  {
+    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())
+    } spell_checker.update(word, include, permanent)
+  }
+
+  def reset_dictionary(): Unit = PIDE.spell_checker.get.foreach(_.reset())
 }
 
diff -r 0f9d2e13187e -r 2b38472a4695 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Mon Apr 14 20:36:50 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Apr 14 21:51:41 2014 +0200
@@ -211,6 +211,11 @@
 isabelle.increase-font-size.shortcut=C+PLUS
 isabelle.increase-font-size2.label=Increase font size (clone)
 isabelle.increase-font-size2.shortcut=C+EQUALS
+isabelle.include-word.label=Include word
+isabelle.include-word-permanently.label=Include word permanently
+isabelle.exclude-word.label=Exclude word
+isabelle.exclude-word-permanently.label=Exclude word permanently
+isabelle.reset-words.label=Reset words
 isabelle.reset-continuous-checking.label=Reset continuous checking
 isabelle.reset-font-size.label=Reset font size
 isabelle.reset-node-required.label=Reset node required
diff -r 0f9d2e13187e -r 2b38472a4695 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 14 20:36:50 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 14 21:51:41 2014 +0200
@@ -176,6 +176,16 @@
     }
 
 
+  /* caret */
+
+  def before_caret_range(text_area: TextArea, rendering: Rendering): Text.Range =
+  {
+    val snapshot = rendering.snapshot
+    val former_caret = snapshot.revert(text_area.getCaretPosition)
+    snapshot.convert(Text.Range(former_caret - 1, former_caret))
+  }
+
+
   /* text ranges */
 
   def buffer_range(buffer: JEditBuffer): Text.Range =
diff -r 0f9d2e13187e -r 2b38472a4695 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Mon Apr 14 20:36:50 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Mon Apr 14 21:51:41 2014 +0200
@@ -17,10 +17,12 @@
 import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
 
+import org.gjt.sp.jedit.textarea.TextArea
+
 
 object Spell_Checker
 {
-  /* marked words within text */
+  /* words within text */
 
   def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean)
     : List[Text.Info[String]] =
@@ -55,6 +57,16 @@
     result.toList
   }
 
+  def current_word(text_area: TextArea, rendering: Rendering): Option[Text.Info[String]] =
+  {
+    val caret = JEdit_Lib.before_caret_range(text_area, rendering)
+    for {
+      spell_range <- rendering.spell_checker_point(caret)
+      text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
+      info <- marked_words(spell_range.start, text, info => info.range.overlaps(caret)).headOption
+    } yield info
+  }
+
 
   /* dictionary declarations */
 
@@ -180,7 +192,7 @@
   }
   load()
 
-  def save()
+  private def save()
   {
     val permanent_decls =
       (for {
@@ -195,30 +207,35 @@
 #
 #   * each line contains at most one word
 #   * extra blanks are ignored
-#   * lines starting with "#" are ignored
+#   * lines starting with "#" are stripped
 #   * lines starting with "-" indicate excluded words
-#   * later entries take precedence
 #
+#:mode=text:encoding=UTF-8:
+
 """
       Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
       File.write(dictionary.user_path, header + cat_lines(permanent_decls))
     }
   }
 
-  def include(word: String, permanent: Boolean)
+  def update(word: String, include: Boolean, permanent: Boolean)
   {
-    declarations += (word -> Spell_Checker.Declaration(true, permanent))
-    if (permanent) save()
+    declarations += (word -> Spell_Checker.Declaration(include, permanent))
+
+    if (include) {
+      if (permanent) save()
 
-    val m = dict.getClass.getDeclaredMethod("add", classOf[String])
-    m.setAccessible(true)
-    m.invoke(dict, word)
+      val m = dict.getClass.getDeclaredMethod("add", classOf[String])
+      m.setAccessible(true)
+      m.invoke(dict, word)
+    }
+    else { save(); load() }
   }
 
-  def exclude(word: String, permanent: Boolean)
+  def reset()
   {
-    declarations += (word -> Spell_Checker.Declaration(false, permanent))
-    save()
+    declarations =
+      declarations -- (for ((name, d) <- declarations.iterator; if !d.permanent) yield name)
     load()
   }