equal
deleted
inserted
replaced
18 import javax.swing.text.Position |
18 import javax.swing.text.Position |
19 import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList} |
19 import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList} |
20 |
20 |
21 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} |
21 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} |
22 import errorlist.DefaultErrorSource |
22 import errorlist.DefaultErrorSource |
23 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, |
23 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} |
24 SideKickCompletionPopup, IAsset} |
|
25 |
24 |
26 |
25 |
27 object Isabelle_Sidekick |
26 object Isabelle_Sidekick |
28 { |
27 { |
29 def int_to_pos(offset: Text.Offset): Position = |
28 def int_to_pos(offset: Text.Offset): Position = |