src/Tools/jEdit/src/completion_popup.scala

       history: Completion.History,
       explicit: Boolean,
       opt_rendering: Option[JEdit_Rendering]): Option[Completion.Result] =
     {
       val buffer = text_area.getBuffer
-      val decode = Isabelle_Encoding.is_active(buffer)
+      val unicode = Isabelle_Encoding.is_active(buffer)
 
       Isabelle.buffer_syntax(buffer) match {
         case Some(syntax) =>
           val context =
             (for {

           val line_start = line_range.start
           for {
             line_text <- JEdit_Lib.try_get_text(buffer, line_range)
             result <-
               syntax.completion.complete(
-                history, decode, explicit, line_start, line_text, caret - line_start, context)
+                history, unicode, explicit, line_start, line_text, caret - line_start, context)
           } yield result
 
         case None => None
       }
     }

       val layered = view.getLayeredPane
       val buffer = text_area.getBuffer
       val painter = text_area.getPainter
 
       val history = PIDE.plugin.completion_history.value
-      val decode = Isabelle_Encoding.is_active(buffer)
+      val unicode = Isabelle_Encoding.is_active(buffer)
 
       def open_popup(result: Completion.Result)
       {
         val font =
           painter.getFont.deriveFont(

         val result0 = syntax_completion(history, explicit, opt_rendering)
         val (no_completion, semantic_completion) =
         {
           opt_rendering match {
             case Some(rendering) =>
-              rendering.semantic_completion_result(history, decode, result0.map(_.range),
+              rendering.semantic_completion_result(history, unicode, result0.map(_.range),
                 JEdit_Lib.before_caret_range(text_area, rendering),
                 JEdit_Lib.try_get_text(buffer, _))
             case None => (false, None)
           }
         }