immler@34393: /*
immler@34393:  * RelativeAsset.scala
immler@34393:  *
immler@34393:  * To change this template, choose Tools | Template Manager
immler@34393:  * and open the template in the editor.
immler@34393:  */
immler@34393: 
immler@34393: package isabelle.prover
immler@34393: 
immler@34393: import sidekick.enhanced.SourceAsset
immler@34393: import javax.swing._
immler@34393: import javax.swing.text.Position
immler@34393: 
immler@34393: class RelativeAsset(base : Command, var rel_start : Int, var rel_end : Int, cons_name : String, desc : String)
immler@34393:       extends SourceAsset {
immler@34393: 
immler@34393: class MyPos(val o : Int) extends Position {
immler@34393:   override def getOffset = o
immler@34393: }
immler@34393:   {
immler@34393:     setStart(new MyPos(base.start + rel_start))
immler@34393:     setEnd(new MyPos(base.start + rel_end))
immler@34393:     setName(cons_name)
immler@34393:     setShort(cons_name)
immler@34393:     setLong(desc)
immler@34393: 
immler@34393:   }
immler@34393: 	/**
immler@34393: 	 * Set the start position
immler@34393: 	 */
immler@34393: 	override def setStart(start : Position) { rel_start = start.getOffset - base.start }
immler@34393: 
immler@34393: 	/**
immler@34393: 	 * Returns the starting position.
immler@34393: 	 */
immler@34393: 	override def getStart : Position = new MyPos(base.start + rel_start)
immler@34393: 
immler@34393: 	/**
immler@34393: 	 * Set the end position
immler@34393: 	 */
immler@34393: 	override def setEnd(end : Position) { rel_end = end.getOffset - base.start }
immler@34393: 
immler@34393: 	/**
immler@34393: 	 * Returns the end position.
immler@34393: 	 */
immler@34393: 	override def getEnd : Position = new MyPos(base.start + rel_end)
immler@34393: 
immler@34393: }