src/Pure/PIDE/rendering.scala
changeset 65139 0a2c0712e432
parent 65133 41f80c6978bc
child 65143 36cd85caf09a
     1.1 --- a/src/Pure/PIDE/rendering.scala	Tue Mar 07 13:55:49 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Tue Mar 07 14:33:14 2017 +0100
     1.3 @@ -169,6 +169,21 @@
     1.4      }
     1.5  
     1.6  
     1.7 +  /* spell checker */
     1.8 +
     1.9 +  private lazy val spell_checker_elements =
    1.10 +    Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
    1.11 +
    1.12 +  def spell_checker_ranges(range: Text.Range): List[Text.Range] =
    1.13 +    snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
    1.14 +
    1.15 +  def spell_checker_point(range: Text.Range): Option[Text.Range] =
    1.16 +    snapshot.select(range, spell_checker_elements, _ =>
    1.17 +      {
    1.18 +        case info => Some(snapshot.convert(info.range))
    1.19 +      }).headOption.map(_.info)
    1.20 +
    1.21 +
    1.22    /* tooltips */
    1.23  
    1.24    def timing_threshold: Double