diff -r 65a247444100 -r 31e9920a0dc1 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Wed Jan 11 16:43:31 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Jan 11 20:01:55 2017 +0100
@@ -39,6 +39,9 @@
 
   /* markup elements */
 
+  private val semantic_completion_elements =
+    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
+
   private val tooltip_descriptions =
     Map(
       Markup.CITATION -> "citation",
@@ -70,6 +73,24 @@
   override def toString: String = "Rendering(" + snapshot.toString + ")"
 
 
+  /* completion */
+
+  def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
+      : Option[Text.Info[Completion.Semantic]] =
+    if (snapshot.is_outdated) None
+    else {
+      snapshot.select(range, Rendering.semantic_completion_elements, _ =>
+        {
+          case Completion.Semantic.Info(info) =>
+            completed_range match {
+              case Some(range0) if range0.contains(info.range) && range0 != info.range => None
+              case _ => Some(info)
+            }
+          case _ => None
+        }).headOption.map(_.info)
+    }
+
+
   /* tooltips */
 
   def tooltip_margin: Int