use isabelle.Completion;

--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Thu Jun 18 19:21:19 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Tue Jun 23 20:16:32 2009 +0200
@@ -52,30 +52,22 @@
   override def complete(pane: EditPane, caret: Int): SideKickCompletion =
   {
     val buffer = pane.getBuffer
-    val ps = Isabelle.prover_setup(buffer)
-    if (ps.isDefined) {
-      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
+    Isabelle.prover_setup(buffer) match {
+      case None => return null
+      case Some(setup) =>
+        val line = buffer.getLineOfOffset(caret)
+        val start = buffer.getLineStartOffset(line)
 
-      val ch = line.charAt(dot - 1)
-      if (!ch.isLetterOrDigit &&   // FIXME Isabelle word!?
-          no_word_sep.indexOf(ch) == -1) return null
+        if (caret == start) return null
+        val text = buffer.getSegment(start, caret - start)
 
-		  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 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
+        setup.prover.complete(text) match {
+          case None => null
+          case Some((word, cs)) =>
+            new SideKickCompletion(pane.getView, word,
+              cs.map(Isabelle.system.symbols.decode(_)).toArray.asInstanceOf[Array[Object]]) { }
+        }
+    }
   }
 
 }

--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Jun 18 19:21:19 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 23 20:16:32 2009 +0200
@@ -76,11 +76,11 @@
   }
 
 
-  /* completions */  // FIXME add symbols, symbol names, symbol abbrevs
+  /* completions */
 
-  var _completions = Scan.Lexicon()
-  def completions(word: CharSequence) = _completions.completions(word)
-  decl_info += (p => _completions += p._1)
+  private var completion = new Completion + isabelle_system.symbols
+  decl_info += (p => completion += p._1)
+  def complete(line: CharSequence): Option[(String, List[String])] = completion.complete(line)
 
 
   /* event handling */