--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Sun Jan 11 22:02:27 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Mon Jan 12 20:49:37 2009 +0100
@@ -7,10 +7,12 @@
package isabelle.jedit
+import scala.collection.Set
+import scala.collection.immutable.TreeSet
import javax.swing.tree.DefaultMutableTreeNode
-import org.gjt.sp.jedit.{Buffer, EditPane}
+import org.gjt.sp.jedit.{Buffer, EditPane, View}
import errorlist.DefaultErrorSource
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion}
@@ -26,18 +28,18 @@
stopped = false
val data = new SideKickParsedData(buffer.getName)
-
- Isabelle.plugin.prover_setup(buffer) match {
- case None =>
- data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
- case Some(prover_setup) =>
- val document = prover_setup.prover.document
+
+ val prover_setup = Isabelle.plugin.prover_setup(buffer)
+ if(prover_setup.isDefined){
+ val document = prover_setup.get.prover.document
val commands = document.commands()
while (!stopped && commands.hasNext) {
data.root.add(commands.next.root_node.swing_node)
}
if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
- }
+ } else {
+ data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
+ }
data
}
@@ -47,6 +49,48 @@
override def supportsCompletion = true
override def canCompleteAnywhere = true
+ override def getInstantCompletionTriggers = "\\"
- override def complete(pane: EditPane, caret: Int): SideKickCompletion = null // TODO
+ 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 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.equals(s)) descriptions.add(s) else descriptions.add(null)
+ }
+ return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
+ } else return 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)
+}