10 import scala.collection.Set |
10 import scala.collection.Set |
11 import scala.collection.immutable.TreeSet |
11 import scala.collection.immutable.TreeSet |
12 |
12 |
13 import javax.swing.tree.DefaultMutableTreeNode |
13 import javax.swing.tree.DefaultMutableTreeNode |
14 |
14 |
15 import org.gjt.sp.jedit.{Buffer, EditPane, View} |
15 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} |
16 import errorlist.DefaultErrorSource |
16 import errorlist.DefaultErrorSource |
17 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion} |
17 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion} |
18 |
18 |
19 |
19 |
20 class IsabelleSideKickParser extends SideKickParser("isabelle") { |
20 class IsabelleSideKickParser extends SideKickParser("isabelle") { |
46 |
46 |
47 /* completion */ |
47 /* completion */ |
48 |
48 |
49 override def supportsCompletion = true |
49 override def supportsCompletion = true |
50 override def canCompleteAnywhere = true |
50 override def canCompleteAnywhere = true |
51 override def getInstantCompletionTriggers = "\\" |
|
52 |
51 |
53 override def complete(pane: EditPane, caret: Int): SideKickCompletion = null /*{ |
52 override def complete(pane: EditPane, caret: Int): SideKickCompletion = |
|
53 { |
54 val buffer = pane.getBuffer |
54 val buffer = pane.getBuffer |
55 val ps = Isabelle.prover_setup(buffer) |
55 val ps = Isabelle.prover_setup(buffer) |
56 if (ps.isDefined) { |
56 if (ps.isDefined) { |
57 val completions = ps.get.prover.completions |
57 val no_word_sep = "_'.?" |
58 def before_caret(i : Int) = buffer.getText(0 max caret - i, i) |
|
59 def next_nonfitting(s : String) : String = { |
|
60 val sa = s.toCharArray |
|
61 sa(s.length - 1) = (sa(s.length - 1) + 1).asInstanceOf[Char] |
|
62 new String(sa) |
|
63 } |
|
64 def suggestions(i : Int) : (Set[String], String)= { |
|
65 val text = before_caret(i) |
|
66 if (!text.matches("\\s") && i < 30) { |
|
67 val larger_results = suggestions(i + 1) |
|
68 if (larger_results._1.size > 0) larger_results |
|
69 else (completions.range(text, next_nonfitting(text)), text) |
|
70 } else (Set[String](), text) |
|
71 |
58 |
72 } |
59 val caret_line = buffer.getLineOfOffset(caret) |
|
60 val line = buffer.getLineSegment(caret_line) |
73 |
61 |
74 val list = new java.util.LinkedList[String] |
62 val dot = caret - buffer.getLineStartOffset(caret_line) |
75 val descriptions = new java.util.LinkedList[String] |
63 if (dot == 0) return null |
76 // compute suggestions |
64 |
77 val (suggs, text) = suggestions(1) |
65 val ch = line.charAt(dot - 1) |
78 for (s <- suggs) { |
66 if (!ch.isLetterOrDigit && // FIXME Isabelle word!? |
79 val decoded = Isabelle.symbols.decode(s) |
67 no_word_sep.indexOf(ch) == -1) return null |
80 list.add(decoded) |
68 |
81 if (decoded != s) descriptions.add(s) else descriptions.add(null) |
69 val word_start = TextUtilities.findWordStart(line, dot - 1, no_word_sep) |
82 } |
70 val word = line.subSequence(word_start, dot) |
83 return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions) |
71 if (word.length <= 1) return null // FIXME property? |
84 } else return null |
72 |
85 }*/ |
73 val completions = ps.get.prover.completions(word).filter(_ != word) |
|
74 if (completions.isEmpty) return null |
|
75 |
|
76 new SideKickCompletion(pane.getView, word.toString, |
|
77 completions.toArray.asInstanceOf[Array[Object]]) {} |
|
78 } else null |
|
79 } |
86 |
80 |
87 } |
81 } |
88 |
|
89 private class IsabelleSideKickCompletion(view: View, text: String, |
|
90 items: java.util.List[String], |
|
91 descriptions : java.util.List[String]) |
|
92 extends SideKickCompletion(view, text, items : java.util.List[String]) { |
|
93 |
|
94 override def getCompletionDescription(i : Int) : String = descriptions.get(i) |
|
95 } |
|