src/Tools/jEdit/src/prover/RelativeAsset.scala
author immler@in.tum.de
Sun Nov 30 19:18:59 2008 +0100 (2008-11-30)
changeset 34393 f0e1608a774f
permissions -rw-r--r--
basic tree structure for sidekick
immler@34393
     1
/*
immler@34393
     2
 * RelativeAsset.scala
immler@34393
     3
 *
immler@34393
     4
 * To change this template, choose Tools | Template Manager
immler@34393
     5
 * and open the template in the editor.
immler@34393
     6
 */
immler@34393
     7
immler@34393
     8
package isabelle.prover
immler@34393
     9
immler@34393
    10
import sidekick.enhanced.SourceAsset
immler@34393
    11
import javax.swing._
immler@34393
    12
import javax.swing.text.Position
immler@34393
    13
immler@34393
    14
class RelativeAsset(base : Command, var rel_start : Int, var rel_end : Int, cons_name : String, desc : String)
immler@34393
    15
      extends SourceAsset {
immler@34393
    16
immler@34393
    17
class MyPos(val o : Int) extends Position {
immler@34393
    18
  override def getOffset = o
immler@34393
    19
}
immler@34393
    20
  {
immler@34393
    21
    setStart(new MyPos(base.start + rel_start))
immler@34393
    22
    setEnd(new MyPos(base.start + rel_end))
immler@34393
    23
    setName(cons_name)
immler@34393
    24
    setShort(cons_name)
immler@34393
    25
    setLong(desc)
immler@34393
    26
immler@34393
    27
  }
immler@34393
    28
	/**
immler@34393
    29
	 * Set the start position
immler@34393
    30
	 */
immler@34393
    31
	override def setStart(start : Position) { rel_start = start.getOffset - base.start }
immler@34393
    32
immler@34393
    33
	/**
immler@34393
    34
	 * Returns the starting position.
immler@34393
    35
	 */
immler@34393
    36
	override def getStart : Position = new MyPos(base.start + rel_start)
immler@34393
    37
immler@34393
    38
	/**
immler@34393
    39
	 * Set the end position
immler@34393
    40
	 */
immler@34393
    41
	override def setEnd(end : Position) { rel_end = end.getOffset - base.start }
immler@34393
    42
immler@34393
    43
	/**
immler@34393
    44
	 * Returns the end position.
immler@34393
    45
	 */
immler@34393
    46
	override def getEnd : Position = new MyPos(base.start + rel_end)
immler@34393
    47
immler@34393
    48
}