--- a/src/Tools/jEdit/etc/options Sat Apr 12 20:49:57 2014 +0200
+++ b/src/Tools/jEdit/etc/options Sat Apr 12 21:00:04 2014 +0200
@@ -57,6 +57,9 @@
public option spell_checker_language : string = "en"
-- "language for spell-checker locale and dictionary (en, de, fr)"
+public option spell_checker_elements : string = "words,ML_comment,SML_comment"
+ -- "relevant markup elements for spell-checker, separated by commas"
+
section "Rendering of Document Content"
--- a/src/Tools/jEdit/src/rendering.scala Sat Apr 12 20:49:57 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Sat Apr 12 21:00:04 2014 +0200
@@ -136,8 +136,6 @@
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
Markup.ML_STRING, Markup.ML_COMMENT)
- private val prose_words_elements = Document.Elements(Markup.WORDS)
-
private val highlight_elements =
Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
@@ -286,10 +284,13 @@
}).headOption.map(_.info)
- /* prose words */
+ /* spell checker */
- def prose_words(range: Text.Range): List[Text.Range] =
- snapshot.select(range, Rendering.prose_words_elements, _ => _ => Some(())).map(_.range)
+ private lazy val spell_checker_elements =
+ Document.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
+
+ def spell_checker_ranges(range: Text.Range): List[Text.Range] =
+ snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
/* command status overview */
--- a/src/Tools/jEdit/src/rich_text_area.scala Sat Apr 12 20:49:57 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Apr 12 21:00:04 2014 +0200
@@ -320,7 +320,7 @@
// spell-checker
for {
spell_checker <- PIDE.get_spell_checker
- range0 <- rendering.prose_words(line_range).iterator
+ range0 <- rendering.spell_checker_ranges(line_range)
text <- JEdit_Lib.try_get_text(buffer, range0)
range <- spell_checker.bad_words(text)
r <- JEdit_Lib.gfx_range(text_area, range + range0.start)