--- 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 */
--- a/src/Pure/Thy/bibtex.scala Thu Nov 26 17:23:33 2020 +0100
+++ b/src/Pure/Thy/bibtex.scala Thu Nov 26 17:32:43 2020 +0100
@@ -191,7 +191,7 @@
models: Map[A, B]): Option[Completion.Result] =
{
for {
- Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret))
+ Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
name1 <- Completion.clean_name(name)
original <- rendering.model.get_text(r)