--- a/src/Pure/PIDE/rendering.scala Fri Jun 09 21:43:31 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala Fri Jun 09 21:57:30 2017 +0200
@@ -223,7 +223,7 @@
def semantic_completion_result(
history: Completion.History,
- decode: Boolean,
+ unicode: Boolean,
completed_range: Option[Text.Range],
caret_range: Text.Range,
try_get_text: Text.Range => Option[String]): (Boolean, Option[Completion.Result]) =
@@ -232,7 +232,7 @@
case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
case Some(Text.Info(range, names: Completion.Names)) =>
try_get_text(range) match {
- case Some(original) => (false, names.complete(range, history, decode, original))
+ case Some(original) => (false, names.complete(range, history, unicode, original))
case None => (false, None)
}
case None => (false, None)