# HG changeset patch
# User wenzelm
# Date 1289478219 -3600
# Node ID 780c272765931f12640616b962a140a8065380bb
# Parent  515eab39b6c2807a15fe4e3e8d150bc431d160ad
tuned;

diff -r 515eab39b6c2 -r 780c27276593 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- 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 =