diff -r 44f9edc5801b -r 7ca1ef2f150d src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Wed Jun 17 00:25:34 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Wed Jun 17 00:26:46 2009 +0200
@@ -12,7 +12,7 @@
 
 import javax.swing.tree.DefaultMutableTreeNode
 
-import org.gjt.sp.jedit.{Buffer, EditPane, View}
+import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
 import errorlist.DefaultErrorSource
 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion}
 
@@ -48,48 +48,34 @@
 
   override def supportsCompletion = true
   override def canCompleteAnywhere = true
-  override def getInstantCompletionTriggers = "\\"
 
-  override def complete(pane: EditPane, caret: Int): SideKickCompletion = null /*{
+  override def complete(pane: EditPane, caret: Int): SideKickCompletion =
+  {
     val buffer = pane.getBuffer
     val ps = Isabelle.prover_setup(buffer)
     if (ps.isDefined) {
-      val completions = ps.get.prover.completions
-      def before_caret(i : Int) = buffer.getText(0 max caret - i, i)
-      def next_nonfitting(s : String) : String = {
-        val sa = s.toCharArray
-        sa(s.length - 1) = (sa(s.length - 1) + 1).asInstanceOf[Char]
-        new String(sa)
-      }
-      def suggestions(i : Int) : (Set[String], String)= {
-        val text = before_caret(i)
-        if (!text.matches("\\s") && i < 30) {
-          val larger_results = suggestions(i + 1)
-          if (larger_results._1.size > 0) larger_results
-          else (completions.range(text, next_nonfitting(text)), text)
-        } else (Set[String](), text)
+      val no_word_sep = "_'.?"
+
+      val caret_line = buffer.getLineOfOffset(caret)
+      val line = buffer.getLineSegment(caret_line)
+
+      val dot = caret - buffer.getLineStartOffset(caret_line)
+      if (dot == 0) return null
+
+      val ch = line.charAt(dot - 1)
+      if (!ch.isLetterOrDigit &&   // FIXME Isabelle word!?
+          no_word_sep.indexOf(ch) == -1) return null
 
-      }
+		  val word_start = TextUtilities.findWordStart(line, dot - 1, no_word_sep)
+      val word = line.subSequence(word_start, dot)
+  		if (word.length <= 1) return null   // FIXME property?
 
-      val list = new java.util.LinkedList[String]
-      val descriptions = new java.util.LinkedList[String]
-      // compute suggestions
-      val (suggs, text) = suggestions(1)
-      for (s <- suggs) {
-        val decoded = Isabelle.symbols.decode(s)
-        list.add(decoded)
-        if (decoded != s) descriptions.add(s) else descriptions.add(null)
-      }
-      return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
-    } else return null
-  }*/
+      val completions = ps.get.prover.completions(word).filter(_ != word)
+      if (completions.isEmpty) return null
+
+      new SideKickCompletion(pane.getView, word.toString,
+        completions.toArray.asInstanceOf[Array[Object]]) {}
+    } else null
+  }
 
 }
-
-private class IsabelleSideKickCompletion(view: View, text: String,
-                                         items: java.util.List[String],
-                                         descriptions : java.util.List[String])
-  extends SideKickCompletion(view, text, items : java.util.List[String]) {
-
-  override def getCompletionDescription(i : Int) : String = descriptions.get(i)
-}