# HG changeset patch
# User wenzelm
# Date 1497038250 -7200
# Node ID 07175635f78c2ed0880e8f9cf885e4010941acdd
# Parent  fb0eea226a4d86f21c903cdab1bc72939d0c0e62
tuned;

diff -r fb0eea226a4d -r 07175635f78c src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Jun 09 21:43:31 2017 +0200
+++ b/src/Pure/General/completion.scala	Fri Jun 09 21:57:30 2017 +0200
@@ -189,10 +189,10 @@
     def complete(
       range: Text.Range,
       history: Completion.History,
-      do_decode: Boolean,
+      unicode: Boolean,
       original: String): Option[Completion.Result] =
     {
-      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
+      def decode(s: String): String = if (unicode) Symbol.decode(s) else s
       val items =
         for {
           (xname, (kind, name)) <- names
@@ -408,14 +408,14 @@
 
   def complete(
     history: Completion.History,
-    do_decode: Boolean,
+    unicode: Boolean,
     explicit: Boolean,
     start: Text.Offset,
     text: CharSequence,
     caret: Int,
     language_context: Completion.Language_Context): Option[Completion.Result] =
   {
-    def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
+    def decode(s: String): String = if (unicode) Symbol.decode(s) else s
     val length = text.length
 
     val abbrevs_result =
diff -r fb0eea226a4d -r 07175635f78c src/Pure/PIDE/rendering.scala
--- 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)
diff -r fb0eea226a4d -r 07175635f78c src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Jun 09 21:43:31 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Jun 09 21:57:30 2017 +0200
@@ -94,7 +94,7 @@
       val line = caret_pos.line
       doc.offset(Line.Position(line)) match {
         case Some(line_start) =>
-          syntax.completion.complete(history, false, true,
+          syntax.completion.complete(history, unicode = false, explicit = true,
             line_start, doc.lines(line).text, caret - line_start, context)
         case None => None
       }
diff -r fb0eea226a4d -r 07175635f78c src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Jun 09 21:43:31 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Jun 09 21:57:30 2017 +0200
@@ -156,7 +156,7 @@
       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) =>
@@ -175,7 +175,7 @@
             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
@@ -294,7 +294,7 @@
       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)
       {
@@ -355,7 +355,7 @@
         {
           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)