--- 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>
--- 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)) =>
--- 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())
}
--- 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
--- 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 =
--- 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()
}