# HG changeset patch
# User wenzelm
# Date 1397329204 -7200
# Node ID d4da2b11c7293cd1716fbc48434a4bb27b10921f
# Parent  b26bdc1f96e51ff6a6941484b8826edac9d27859
more general spell_checker_elements;

diff -r b26bdc1f96e5 -r d4da2b11c729 src/Tools/jEdit/etc/options
--- 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"
 
diff -r b26bdc1f96e5 -r d4da2b11c729 src/Tools/jEdit/src/rendering.scala
--- 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 */
diff -r b26bdc1f96e5 -r d4da2b11c729 src/Tools/jEdit/src/rich_text_area.scala
--- 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)