src/Pure/PIDE/rendering.scala
changeset 66114 c137a9f038a6
parent 66074 4329cc78c2a1
child 66117 e6f808d1307c
--- a/src/Pure/PIDE/rendering.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -209,6 +209,8 @@
 {
   override def toString: String = "Rendering(" + snapshot.toString + ")"
 
+  def model: Document.Model
+
 
   /* completion */
 
@@ -231,13 +233,12 @@
     history: Completion.History,
     unicode: Boolean,
     completed_range: Option[Text.Range],
-    caret_range: Text.Range,
-    try_get_text: Text.Range => Option[String]): (Boolean, Option[Completion.Result]) =
+    caret_range: Text.Range): (Boolean, Option[Completion.Result]) =
   {
     semantic_completion(completed_range, caret_range) match {
       case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
       case Some(Text.Info(range, names: Completion.Names)) =>
-        try_get_text(range) match {
+        model.try_get_text(range) match {
           case Some(original) => (false, names.complete(range, history, unicode, original))
           case None => (false, None)
         }