--- a/src/Pure/PIDE/rendering.scala Thu Nov 26 17:23:33 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala Thu Nov 26 17:32:43 2020 +0100
@@ -296,13 +296,13 @@
Some(Completion.Language_Context.inner)
}).headOption.map(_.info)
- def citation(range: Text.Range): Option[Text.Info[String]] =
+ def citations(range: Text.Range): List[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)
+ }).map(_.info)
/* file-system path completion */