11 import isabelle._ |
11 import isabelle._ |
12 |
12 |
13 import scala.collection.Set |
13 import scala.collection.Set |
14 import scala.collection.immutable.TreeSet |
14 import scala.collection.immutable.TreeSet |
15 |
15 |
|
16 import java.awt.Component |
16 import javax.swing.tree.DefaultMutableTreeNode |
17 import javax.swing.tree.DefaultMutableTreeNode |
17 import javax.swing.text.Position |
18 import javax.swing.text.Position |
18 import javax.swing.Icon |
19 import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList} |
19 |
20 |
20 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} |
21 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} |
21 import errorlist.DefaultErrorSource |
22 import errorlist.DefaultErrorSource |
22 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} |
23 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, |
|
24 SideKickCompletionPopup, IAsset} |
23 |
25 |
24 |
26 |
25 object Isabelle_Sidekick |
27 object Isabelle_Sidekick |
26 { |
28 { |
27 def int_to_pos(offset: Text.Offset): Position = |
29 def int_to_pos(offset: Text.Offset): Position = |
99 val ds = |
101 val ds = |
100 (if (Isabelle_Encoding.is_active(buffer)) |
102 (if (Isabelle_Encoding.is_active(buffer)) |
101 cs.map(Symbol.decode(_)).sorted |
103 cs.map(Symbol.decode(_)).sorted |
102 else cs).filter(_ != word) |
104 else cs).filter(_ != word) |
103 if (ds.isEmpty) null |
105 if (ds.isEmpty) null |
104 else new SideKickCompletion( |
106 else |
105 pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } |
107 new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { |
|
108 override def getRenderer() = |
|
109 new ListCellRenderer[Any] { |
|
110 val default_renderer = |
|
111 (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]] |
|
112 |
|
113 override def getListCellRendererComponent( |
|
114 list: JList[_ <: Any], value: Any, index: Int, |
|
115 selected: Boolean, focus: Boolean): Component = |
|
116 { |
|
117 val renderer: Component = |
|
118 default_renderer.getListCellRendererComponent( |
|
119 list, value, index, selected, focus) |
|
120 renderer.setFont(pane.getTextArea.getPainter.getFont) |
|
121 renderer |
|
122 } |
|
123 } |
|
124 } |
106 } |
125 } |
107 } |
126 } |
108 } |
127 } |
109 } |
128 } |
110 } |
129 } |