src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
changeset 38426 2858ec7b6dd8
parent 38417 b8922ae21111
child 38479 e628da370072
     1.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 15 21:42:13 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 15 22:48:56 2010 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4      for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
     1.5        root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
     1.6            {
     1.7 -            val content = command.source(node.start, node.stop).replace('\n', ' ')
     1.8 +            val content = command.source(node.range).replace('\n', ' ')
     1.9              val id = command.id
    1.10  
    1.11              new DefaultMutableTreeNode(new IAsset {
    1.12 @@ -141,9 +141,9 @@
    1.13                override def getName: String = Markup.Long(id)
    1.14                override def setName(name: String) = ()
    1.15                override def setStart(start: Position) = ()
    1.16 -              override def getStart: Position = command_start + node.start
    1.17 +              override def getStart: Position = command_start + node.range.start
    1.18                override def setEnd(end: Position) = ()
    1.19 -              override def getEnd: Position = command_start + node.stop
    1.20 +              override def getEnd: Position = command_start + node.range.stop
    1.21                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    1.22              })
    1.23            }))