src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
changeset 40477 780c27276593
parent 40475 8a57ff2c2600
child 40792 1d71a45590e4
--- 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 =