src/Tools/jEdit/src/completion_popup.scala

--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 18:07:35 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 20:15:47 2014 +0100
@@ -92,6 +92,65 @@
       }
 
 
+    /* rendering */
+
+    def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
+    {
+      active_range match {
+        case Some(range) => range.try_restrict(line_range)
+        case None =>
+          val buffer = text_area.getBuffer
+          val caret = text_area.getCaretPosition
+
+          if (line_range.contains(caret)) {
+            JEdit_Lib.stretch_point_range(buffer, caret).try_restrict(line_range) match {
+              case Some(range) if !range.is_singularity =>
+                rendering.completion_names(range) match {
+                  case Some(names) => Some(names.range)
+                  case None =>
+                    syntax_completion(Some(rendering), false) match {
+                      case Some(result) => Some(result.range)
+                      case None => None
+                    }
+                }
+              case _ => None
+            }
+          }
+          else None
+      }
+    }.map(range => Text.Info(range, rendering.completion_color))
+
+
+    /* syntax completion */
+
+    def syntax_completion(
+      opt_rendering: Option[Rendering], explicit: Boolean): Option[Completion.Result] =
+    {
+      val buffer = text_area.getBuffer
+      val history = PIDE.completion_history.value
+      val decode = Isabelle_Encoding.is_active(buffer)
+
+      Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
+        case Some(syntax) =>
+          val caret = text_area.getCaretPosition
+          val line = buffer.getLineOfOffset(caret)
+          val start = buffer.getLineStartOffset(line)
+          val text = buffer.getSegment(start, caret - start)
+
+          val context =
+            (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
+              case Some(rendering) =>
+                rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
+              case None => None
+            }) getOrElse syntax.completion_context
+
+          syntax.completion.complete(history, decode, explicit, start, text, context)
+
+        case None => None
+      }
+    }
+
+
     /* completion action */
 
     private def insert(item: Completion.Item)
@@ -179,41 +238,20 @@
           }
         }
 
-      def syntax_completion(): Boolean =
-      {
-        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
-          case Some(syntax) =>
-            val line = buffer.getLineOfOffset(caret)
-            val start = buffer.getLineStartOffset(line)
-            val text = buffer.getSegment(start, caret - start)
-
-            val context =
-              (PIDE.document_view(text_area) match {
-                case None => None
-                case Some(doc_view) =>
-                  val rendering = doc_view.get_rendering()
-                  rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
-              }) getOrElse syntax.completion_context
-
-            syntax.completion.complete(history, decode, explicit, start, text, context) match {
-              case Some(result) =>
-                result.items match {
-                  case List(item) if result.unique && item.immediate && immediate =>
-                    insert(item)
-                    true
-                  case _ :: _ =>
-                    open_popup(result)
-                    true
-                  case _ => false
-                }
-              case None => false
+      def syntactic_completion(): Boolean =
+        syntax_completion(None, explicit) match {
+          case Some(result) =>
+            result.items match {
+              case List(item) if result.unique && item.immediate && immediate =>
+                insert(item); true
+              case _ :: _ => open_popup(result); true
+              case _ => false
             }
           case None => false
         }
-      }
 
       if (buffer.isEditable)
-        semantic_completion() || syntax_completion()
+        semantic_completion() || syntactic_completion()
     }