src/Pure/PIDE/rendering.scala

--- a/src/Pure/PIDE/rendering.scala	Tue Mar 07 13:55:49 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Tue Mar 07 14:33:14 2017 +0100
@@ -169,6 +169,21 @@
     }
 
 
+  /* spell checker */
+
+  private lazy val spell_checker_elements =
+    Markup.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)
+
+  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)
+
+
   /* tooltips */
 
   def timing_threshold: Double