more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;

--- a/NEWS	Tue Jan 09 20:03:14 2018 +0100
+++ b/NEWS	Tue Jan 09 20:15:36 2018 +0100
@@ -51,6 +51,10 @@
 
 *** Isabelle/jEdit Prover IDE ***
 
+* System options "spell_checker_include" and "spell_checker_exclude"
+supersede former "spell_checker_elements" to determine regions of text
+that are subject to spell-checking. Minor INCOMPATIBILITY.
+
 * PIDE markup for session ROOT files: allows to complete session names,
 follow links to theories and document files etc.
 

--- a/etc/options	Tue Jan 09 20:03:14 2018 +0100
+++ b/etc/options	Tue Jan 09 20:15:36 2018 +0100
@@ -214,8 +214,11 @@
 public option spell_checker_dictionary : string = "en"
   -- "spell-checker dictionary name"
 
-public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
-  -- "relevant markup elements for spell-checker, separated by commas"
+public option spell_checker_include : string = "words,comment,inner_comment,ML_comment,SML_comment"
+  -- "included markup elements for spell-checker (separated by commas)"
+
+public option spell_checker_exclude : string = "antiquoted"
+  -- "excluded markup elements for spell-checker (separated by commas)"
 
 
 section "Secure Shell"

--- a/src/Doc/JEdit/JEdit.thy	Tue Jan 09 20:03:14 2018 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Tue Jan 09 20:15:36 2018 +0100
@@ -1673,9 +1673,13 @@
   permanent dictionary updates is stored in the directory @{path
   "$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary.
 
-  \<^item> @{system_option_def spell_checker_elements} specifies a comma-separated
+  \<^item> @{system_option_def spell_checker_include} specifies a comma-separated
   list of markup elements that delimit words in the source that is subject to
   spell-checking, including various forms of comments.
+
+  \<^item> @{system_option_def spell_checker_exclude} specifies a comma-separated
+  list of markup elements that disable spell-checking (e.g.\ in nested
+  antiquotations).
 \<close>
 
 

--- a/src/Pure/PIDE/rendering.scala	Tue Jan 09 20:03:14 2018 +0100
+++ b/src/Pure/PIDE/rendering.scala	Tue Jan 09 20:15:36 2018 +0100
@@ -355,17 +355,30 @@
 
   /* spell checker */
 
+  private lazy val spell_checker_include =
+    Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*)
+
   private lazy val spell_checker_elements =
-    Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
+    spell_checker_include ++
+      Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
 
-  def spell_checker_ranges(range: Text.Range): List[Text.Range] =
-    snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
+  def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] =
+  {
+    val result =
+      snapshot.select(range, spell_checker_elements, _ =>
+        {
+          case info =>
+            Some(
+              if (spell_checker_include(info.info.name))
+                Some(snapshot.convert(info.range))
+              else None)
+        })
+    for (Text.Info(range, Some(range1)) <- result)
+      yield Text.Info(range, range1)
+  }
 
   def spell_checker_point(range: Text.Range): Option[Text.Range] =
-    snapshot.select(range, spell_checker_elements, _ =>
-      {
-        case info => Some(snapshot.convert(info.range))
-      }).headOption.map(_.info)
+    spell_checker(range).headOption.map(_.info)
 
 
   /* text background */

--- a/src/Tools/VSCode/src/vscode_spell_checker.scala	Tue Jan 09 20:03:14 2018 +0100
+++ b/src/Tools/VSCode/src/vscode_spell_checker.scala	Tue Jan 09 20:15:36 2018 +0100
@@ -18,9 +18,9 @@
     val ranges =
       (for {
         spell_checker <- rendering.resources.spell_checker.get.iterator
-        spell_range <- rendering.spell_checker_ranges(model.content.text_range).iterator
-        text <- model.get_text(spell_range).iterator
-        info <- spell_checker.marked_words(spell_range.start, text).iterator
+        spell <- rendering.spell_checker(model.content.text_range).iterator
+        text <- model.get_text(spell.range).iterator
+        info <- spell_checker.marked_words(spell.range.start, text).iterator
       } yield info.range).toList
     Document_Model.Decoration.ranges("spell_checker", ranges)
   }

--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Jan 09 20:03:14 2018 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Jan 09 20:15:36 2018 +0100
@@ -344,9 +344,9 @@
             // spell checker
             for {
               spell_checker <- PIDE.plugin.spell_checker.get
-              spell_range <- rendering.spell_checker_ranges(line_range)
-              text <- JEdit_Lib.get_text(buffer, spell_range)
-              info <- spell_checker.marked_words(spell_range.start, text)
+              spell <- rendering.spell_checker(line_range)
+              text <- JEdit_Lib.get_text(buffer, spell.range)
+              info <- spell_checker.marked_words(spell.range.start, text)
               r <- JEdit_Lib.gfx_range(text_area, info.range)
             } {
               gfx.setColor(rendering.spell_checker_color)