# HG changeset patch
# User wenzelm
# Date 1245782996 -7200
# Node ID 5a03dc7a19e17590e6eea337e1bf2cfd461702c2
# Parent  b40e43d70ae94cefeed8e1c586e3bd30e322af72
fall back on Isabelle system completion (symbols only);
tuned;

diff -r b40e43d70ae9 -r 5a03dc7a19e1 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Tue Jun 23 20:16:32 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Tue Jun 23 20:49:56 2009 +0200
@@ -52,21 +52,19 @@
   override def complete(pane: EditPane, caret: Int): SideKickCompletion =
   {
     val buffer = pane.getBuffer
-    Isabelle.prover_setup(buffer) match {
-      case None => return null
-      case Some(setup) =>
-        val line = buffer.getLineOfOffset(caret)
-        val start = buffer.getLineStartOffset(line)
+
+    val line = buffer.getLineOfOffset(caret)
+    val start = buffer.getLineStartOffset(line)
+    val text = buffer.getSegment(start, caret - start)
 
-        if (caret == start) return null
-        val text = buffer.getSegment(start, caret - start)
+    val completion =
+      Isabelle.prover_setup(buffer).map(_.prover.completion) getOrElse Isabelle.completion
 
-        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]]) { }
-        }
+    completion.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 b40e43d70ae9 -r 5a03dc7a19e1 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Jun 23 20:16:32 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Jun 23 20:49:56 2009 +0200
@@ -38,6 +38,7 @@
   // Isabelle system instance
   var system: IsabelleSystem = null
   def symbols = system.symbols
+  lazy val completion = new Completion + symbols
 
   // settings
   def default_logic = {
diff -r b40e43d70ae9 -r 5a03dc7a19e1 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 23 20:16:32 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 23 20:49:56 2009 +0200
@@ -78,9 +78,9 @@
 
   /* completions */
 
-  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)
+  private var _completion = Isabelle.completion
+  def completion = _completion
+  decl_info += (p => _completion += p._1)
 
 
   /* event handling */