# HG changeset patch
# User wenzelm
# Date 1377629102 -7200
# Node ID 4b422e5d64fdcbb3d284b7289a61f093bccc28f4
# Parent  4a37626934529c4797b905919fa1ecd2a3732d1f
some actual completion via outer syntax;
disable old SideKick completion for "isabelle" mode;

diff -r 4a3762693452 -r 4b422e5d64fd src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 17:17:20 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 20:45:02 2013 +0200
@@ -22,46 +22,83 @@
 
 object Completion_Popup
 {
-  sealed case class Item(name: String, text: String)
-  { override def toString: String = text }
+  private sealed case class Item(original: String, replacement: String, description: String)
+  { override def toString: String = description }
+
+  private def complete_item(text_area: JEditTextArea, item: Item)
+  {
+    Swing_Thread.require()
 
-  def input_text_area(text_area: JEditTextArea, evt: KeyEvent)
+    val buffer = text_area.getBuffer
+    val len = item.original.length
+    if (buffer.isEditable && len > 0) {
+      JEdit_Lib.buffer_edit(buffer) {
+        val caret = text_area.getCaretPosition
+        JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match {
+          case Some(text) if text == item.original =>
+            buffer.remove(caret - len, len)
+            buffer.insert(caret - len, item.replacement)
+          case _ =>
+        }
+      }
+    }
+  }
+
+  def input_text_area(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax], evt: KeyEvent)
   {
     Swing_Thread.require()
 
     val buffer = text_area.getBuffer
     if (buffer.isEditable) {
-      val view = text_area.getView
-      val painter = text_area.getPainter
-      val caret = text_area.getCaretPosition
+      get_syntax match {
+        case None =>
+        case Some(syntax) =>
+          val view = text_area.getView
+          val painter = text_area.getPainter
 
-      // FIXME
-      def complete(item: Item) { }
-
-      // FIXME
-      val token_length = 0
-      val items: List[Item] = Nil
+          val caret = text_area.getCaretPosition
+          val completion =
+          {
+            val line = buffer.getLineOfOffset(caret)
+            val start = buffer.getLineStartOffset(line)
+            val text = buffer.getSegment(start, caret - start)
 
-      val popup_font =
-        painter.getFont.deriveFont(
-          (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
-            max 10.0f)
+            syntax.completion.complete(text) match {
+              case None => None
+              case Some((word, cs)) =>
+                val ds =
+                  (if (Isabelle_Encoding.is_active(buffer))
+                    cs.map(Symbol.decode(_)).sorted
+                   else cs).filter(_ != word)
+                if (ds.isEmpty) None
+                else Some((word, ds.map(s => Item(word, s, s))))
+            }
+          }
+          completion match {
+            case None =>
+            case Some((original, items)) =>
+              val popup_font =
+                painter.getFont.deriveFont(
+                  (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
+                    max 10.0f)
 
-      if (!items.isEmpty) {
-        val location = text_area.offsetToXY(caret - token_length)
-        if (location != null) {
-          location.y = location.y + painter.getFontMetrics.getHeight
-          SwingUtilities.convertPointToScreen(location, painter)
-          new Completion_Popup(view.getRootPane, popup_font, location, items) {
-            override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) }
-            override def hidden() { text_area.requestFocus }
+              val location = text_area.offsetToXY(caret - original.length)
+              if (location != null) {
+                location.y = location.y + painter.getFontMetrics.getHeight
+                SwingUtilities.convertPointToScreen(location, painter)
+                new Completion_Popup(view.getRootPane, popup_font, location, items) {
+                  override def complete(item: Item) { complete_item(text_area, item) }
+                  override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) }
+                  override def hidden() { text_area.requestFocus }
+                }
+              }
           }
-        }
       }
     }
   }
 }
 
+
 class Completion_Popup private(
   root: JComponent,
   popup_font: Font,
diff -r 4a3762693452 -r 4b422e5d64fd src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 17:17:20 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 20:45:02 2013 +0200
@@ -151,7 +151,7 @@
 
   private val key_listener =
     JEdit_Lib.key_listener(
-      key_typed = Completion_Popup.input_text_area(text_area, _),
+      key_typed = Completion_Popup.input_text_area(text_area, PIDE.get_recent_syntax, _),
       key_pressed = (evt: KeyEvent) =>
         {
           if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())
diff -r 4a3762693452 -r 4b422e5d64fd src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 27 17:17:20 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 27 20:45:02 2013 +0200
@@ -188,6 +188,9 @@
 
 class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
   "isabelle", PIDE.get_recent_syntax, PIDE.thy_load.buffer_node_name)
+{
+  override def supportsCompletion = false
+}
 
 
 class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(