--- 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]]) { }
}
}
--- 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 = {
--- 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 */