try explicit semantic completion before syntax completion;

--- a/src/Pure/General/completion.scala	Sun Feb 23 19:29:27 2014 +0100
+++ b/src/Pure/General/completion.scala	Sun Feb 23 20:24:33 2014 +0100
@@ -32,6 +32,23 @@
   }
 
   sealed case class Names(range: Text.Range, total: Int, names: List[String])
+  {
+    def complete(
+      history: Completion.History,
+      decode: Boolean,
+      original: String): Option[Completion.Result] =
+    {
+      val items =
+        for {
+          raw_name <- names
+          name = (if (decode) Symbol.decode(raw_name) else raw_name)
+          if name != original
+        } yield Item(range, original, name, name, 0, true)
+
+      if (items.isEmpty) None
+      else Some(Result(range, original, names.length == 1, items))
+    }
+  }
 
 
 
@@ -64,7 +81,11 @@
     immediate: Boolean)
   { override def toString: String = name }
 
-  sealed case class Result(original: String, unique: Boolean, items: List[Item])
+  sealed case class Result(
+    range: Text.Range,
+    original: String,
+    unique: Boolean,
+    items: List[Item])
 
 
   /* init */
@@ -278,6 +299,7 @@
 
     words_result match {
       case Some((word, cs)) =>
+        val range = Text.Range(- word.length, 0) + (text_start + text.length)
         val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
         if (ds.isEmpty) None
         else {
@@ -291,10 +313,9 @@
                   case List(s1, s2) => (s1, s2)
                   case _ => (s, "")
                 }
-              val range = Text.Range(- word.length, 0) + (text_start + text.length)
               Completion.Item(range, word, s, s1 + s2, - s2.length, explicit || immediate)
             })
-          Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering)))
+          Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
         }
       case None => None
     }

--- a/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 19:29:27 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Feb 23 20:24:33 2014 +0100
@@ -99,17 +99,70 @@
       val layered = view.getLayeredPane
       val buffer = text_area.getBuffer
       val painter = text_area.getPainter
+      val caret = text_area.getCaretPosition
 
-      if (buffer.isEditable) {
+      val history = PIDE.completion_history.value
+      val decode = Isabelle_Encoding.is_active(buffer)
+
+      def open_popup(result: Completion.Result)
+      {
+        val font =
+          painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+
+        val loc1 = text_area.offsetToXY(result.range.start)
+        if (loc1 != null) {
+          val loc2 =
+            SwingUtilities.convertPoint(painter,
+              loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
+
+          val completion =
+            new Completion_Popup(layered, loc2, font, result.items) {
+              override def complete(item: Completion.Item) {
+                PIDE.completion_history.update(item)
+                insert(item)
+              }
+              override def propagate(evt: KeyEvent) {
+                JEdit_Lib.propagate_key(view, evt)
+                input(evt)
+              }
+              override def refocus() { text_area.requestFocus }
+            }
+          completion_popup = Some(completion)
+          completion.show_popup()
+        }
+      }
+
+      def semantic_completion(): Boolean =
+        explicit && {
+          PIDE.document_view(text_area) match {
+            case Some(doc_view) =>
+              val rendering = doc_view.get_rendering()
+              rendering.completion_names(JEdit_Lib.stretch_point_range(buffer, caret)) match {
+                case None => false
+                case Some(names) =>
+                  JEdit_Lib.try_get_text(buffer, names.range) match {
+                    case Some(original) =>
+                      names.complete(history, decode, original) match {
+                        case Some(result) if !result.items.isEmpty =>
+                          open_popup(result)
+                          true
+                        case _ => false
+                      }
+                    case None => false
+                  }
+              }
+            case _ => false
+          }
+        }
+
+      def syntax_completion(): Boolean =
+      {
         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 history = PIDE.completion_history.value
-            val decode = Isabelle_Encoding.is_active(buffer)
             val context =
               (PIDE.document_view(text_area) match {
                 case None => None
@@ -120,39 +173,23 @@
 
             syntax.completion.complete(history, decode, explicit, start, text, context) match {
               case Some(result) =>
-                if (result.unique && result.items.head.immediate && immediate)
-                  insert(result.items.head)
-                else {
-                  val font =
-                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
-
-                  val loc1 = text_area.offsetToXY(caret - result.original.length)
-                  if (loc1 != null) {
-                    val loc2 =
-                      SwingUtilities.convertPoint(painter,
-                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
-
-                    val completion =
-                      new Completion_Popup(layered, loc2, font, result.items) {
-                        override def complete(item: Completion.Item) {
-                          PIDE.completion_history.update(item)
-                          insert(item)
-                        }
-                        override def propagate(evt: KeyEvent) {
-                          JEdit_Lib.propagate_key(view, evt)
-                          input(evt)
-                        }
-                        override def refocus() { text_area.requestFocus }
-                      }
-                    completion_popup = Some(completion)
-                    completion.show_popup()
-                  }
+                result.items match {
+                  case List(item) if result.unique && item.immediate && immediate =>
+                    insert(item)
+                    true
+                  case _ :: _ =>
+                    open_popup(result)
+                    true
+                  case _ => false
                 }
-              case None =>
+              case None => false
             }
-          case None =>
+          case None => false
         }
       }
+
+      if (buffer.isEditable)
+        semantic_completion() || syntax_completion()
     }