# HG changeset patch
# User immler@in.tum.de
# Date 1247658561 -7200
# Node ID 2740439a86b4ed5576acf43ee10ad6c766ab2a88
# Parent  77722b866fb47b1a8ff12a890c4c9f88c237c603
decode offsets with respect to symbols

diff -r 77722b866fb4 -r 2740439a86b4 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Wed Jul 15 13:13:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Wed Jul 15 13:49:21 2009 +0200
@@ -95,7 +95,9 @@
     new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
       Nil, id, content, RootInfo())
   private var _markup_root = empty_root_node
-  def add_markup(state: IsarDocument.State_ID, node: MarkupNode) = {
+  def add_markup(state: IsarDocument.State_ID, raw_node: MarkupNode) = {
+    // decode node
+    val node = raw_node transform symbol_index.decode
     if (state == null) _markup_root = _markup_root.add(node)
     else {
       val cmd_state = states.getOrElseUpdate(state, new Command_State(this))
diff -r 77722b866fb4 -r 2740439a86b4 src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed Jul 15 13:13:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed Jul 15 13:49:21 2009 +0200
@@ -55,6 +55,10 @@
   val children: List[MarkupNode],
   val id: String, val content: String, val info: MarkupInfo)
 {
+
+  def transform(f: Int => Int): MarkupNode = new MarkupNode(base,
+    f(start), f(stop), children map (_ transform f), id, content, info)
+
   def swing_node(doc: ProofDocument): DefaultMutableTreeNode = {
     val node = MarkupNode.markup2default_node (this, base, doc)
     children.map(node add _.swing_node(doc))