--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Nov 11 13:07:41 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Nov 11 13:23:39 2010 +0100
@@ -24,10 +24,10 @@
object Isabelle_Sidekick
{
- def int_to_pos(offset: Int): Position =
+ def int_to_pos(offset: Text.Offset): Position =
new Position { def getOffset = offset; override def toString = offset.toString }
- class Asset(name: String, start: Int, end: Int) extends IAsset
+ class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
{
protected var _name = name
protected var _start = int_to_pos(start)
@@ -79,7 +79,7 @@
override def supportsCompletion = true
override def canCompleteAnywhere = true
- override def complete(pane: EditPane, caret: Int): SideKickCompletion =
+ override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
{
val buffer = pane.getBuffer
Isabelle.swing_buffer_lock(buffer) {
@@ -116,7 +116,7 @@
{
val syntax = model.session.current_syntax()
- def make_tree(offset: Int, entry: Structure.Entry): List[DefaultMutableTreeNode] =
+ def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
entry match {
case Structure.Block(name, body) =>
val node =