50 override def canCompleteAnywhere = true |
50 override def canCompleteAnywhere = true |
51 |
51 |
52 override def complete(pane: EditPane, caret: Int): SideKickCompletion = |
52 override def complete(pane: EditPane, caret: Int): SideKickCompletion = |
53 { |
53 { |
54 val buffer = pane.getBuffer |
54 val buffer = pane.getBuffer |
55 Isabelle.prover_setup(buffer) match { |
|
56 case None => return null |
|
57 case Some(setup) => |
|
58 val line = buffer.getLineOfOffset(caret) |
|
59 val start = buffer.getLineStartOffset(line) |
|
60 |
55 |
61 if (caret == start) return null |
56 val line = buffer.getLineOfOffset(caret) |
62 val text = buffer.getSegment(start, caret - start) |
57 val start = buffer.getLineStartOffset(line) |
|
58 val text = buffer.getSegment(start, caret - start) |
63 |
59 |
64 setup.prover.complete(text) match { |
60 val completion = |
65 case None => null |
61 Isabelle.prover_setup(buffer).map(_.prover.completion) getOrElse Isabelle.completion |
66 case Some((word, cs)) => |
62 |
67 new SideKickCompletion(pane.getView, word, |
63 completion.complete(text) match { |
68 cs.map(Isabelle.system.symbols.decode(_)).toArray.asInstanceOf[Array[Object]]) { } |
64 case None => null |
69 } |
65 case Some((word, cs)) => |
|
66 new SideKickCompletion(pane.getView, word, |
|
67 cs.map(Isabelle.system.symbols.decode(_)).toArray.asInstanceOf[Array[Object]]) { } |
70 } |
68 } |
71 } |
69 } |
72 |
70 |
73 } |
71 } |