# HG changeset patch
# User wenzelm
# Date 1606408363 -3600
# Node ID 83411077c37be8c1e7bd96709932c0cb06b094e1
# Parent  caa182bdab7aa55de240af332249e7072679bdbd
clarified signature;

diff -r caa182bdab7a -r 83411077c37b src/Pure/PIDE/rendering.scala
--- 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 */
diff -r caa182bdab7a -r 83411077c37b src/Pure/Thy/bibtex.scala
--- 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)