# HG changeset patch
# User immler@in.tum.de
# Date 1228658497 -3600
# Node ID de809360c51d157907017c1f8747e1ecc4383da2
# Parent  287f3ecdfc2ad8075520582e5e55a47311e76a48
command property: offset relative to start of command

diff -r 287f3ecdfc2a -r de809360c51d src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Dec 02 15:25:24 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sun Dec 07 15:01:37 2008 +0100
@@ -73,6 +73,7 @@
     val cand_asset = cand.getUserObject.asInstanceOf[RelativeAsset]
     val c_start = cand_asset.rel_start
     val c_end = cand_asset.rel_end
+    System.err.println(c_start - n_start + " " + (c_end - n_end))
     return c_start >= n_start && c_end <= n_end
   }
 
@@ -105,18 +106,20 @@
     var markup_begin = -1
     var markup_end = -1
     for((n, a) <- attr) {
-      if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - first.start
-      if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - first.start
+      if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - 1
+      if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - 1
     }
     if(markup_begin > -1 && markup_end > -1){
       statuses = new Status(markup_info, markup_begin, markup_end) :: statuses
-      val content = Plugin.plugin.prover.document.getContent(this).substring(markup_begin, markup_end)
-      val asset = new RelativeAsset(this, markup_begin, markup_end, markup_info, content)
+      val markup_content = content.substring(markup_begin, markup_end)
+      val asset = new RelativeAsset(this, markup_begin, markup_end, markup_info, markup_content)
       val new_node = new DefaultMutableTreeNode(asset)
       insert_node(new_node, root_node)
     }
   }
 
+  def content = Plugin.plugin.prover.document.getContent(this)
+
   def next = if (last.next != null) last.next.command else null
   def previous = if (first.previous != null) first.previous.command else null
 
diff -r 287f3ecdfc2a -r de809360c51d src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Dec 02 15:25:24 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Dec 07 15:01:37 2008 +0100
@@ -174,7 +174,7 @@
     
     val props = new Properties()
     props.setProperty("id", cmd.idString)
-    props.setProperty("offset", Integer.toString(cmd.first.start))
+    props.setProperty("offset", Integer.toString(1))
 
     val content = converter.encode(document.getContent(cmd))
     process.output_sync("Isar.command "