equal
deleted
inserted
replaced
246 snapshot.select(range, JEdit_Rendering.citation_elements, _ => |
246 snapshot.select(range, JEdit_Rendering.citation_elements, _ => |
247 { |
247 { |
248 case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => |
248 case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => |
249 Some(Text.Info(snapshot.convert(info_range), name)) |
249 Some(Text.Info(snapshot.convert(info_range), name)) |
250 case _ => None |
250 case _ => None |
251 }).headOption.map(_.info) |
|
252 |
|
253 |
|
254 /* spell checker */ |
|
255 |
|
256 private lazy val spell_checker_elements = |
|
257 Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*) |
|
258 |
|
259 def spell_checker_ranges(range: Text.Range): List[Text.Range] = |
|
260 snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range) |
|
261 |
|
262 def spell_checker_point(range: Text.Range): Option[Text.Range] = |
|
263 snapshot.select(range, spell_checker_elements, _ => |
|
264 { |
|
265 case info => Some(snapshot.convert(info.range)) |
|
266 }).headOption.map(_.info) |
251 }).headOption.map(_.info) |
267 |
252 |
268 |
253 |
269 /* breakpoints */ |
254 /* breakpoints */ |
270 |
255 |