--- a/src/Tools/jEdit/src/rendering.scala Mon Oct 06 14:21:38 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Mon Oct 06 16:54:35 2014 +0200
@@ -138,6 +138,8 @@
private val language_elements = Markup.Elements(Markup.LANGUAGE)
+ private val citation_elements = Markup.Elements(Markup.CITATION)
+
private val highlight_elements =
Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
@@ -296,6 +298,14 @@
case _ => None
}).headOption.map(_.info)
+ def citation(range: Text.Range): Option[Text.Info[String]] =
+ snapshot.select(range, Rendering.citation_elements, _ =>
+ {
+ case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
+ Some(Text.Info(snapshot.convert(info_range), name))
+ case _ => None
+ }).headOption.map(_.info)
+
/* spell checker */