--- 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)
-}