# HG changeset patch
# User wenzelm
# Date 1245780992 -7200
# Node ID b40e43d70ae94cefeed8e1c586e3bd30e322af72
# Parent  14e4d83f100017cea6274dfc11d0aa363ac2a005
use isabelle.Completion;

diff -r 14e4d83f1000 -r b40e43d70ae9 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- 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]]) { }
+        }
+    }
   }
 
 }
diff -r 14e4d83f1000 -r b40e43d70ae9 src/Tools/jEdit/src/prover/Prover.scala
--- 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 */