--- a/src/Tools/jEdit/build.xml Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/build.xml Mon Mar 02 19:27:06 2009 +0100
@@ -72,4 +72,22 @@
<copy file="plugin/actions.xml" todir="${build.classes.dir}" />
<copy file="plugin/Isabelle.props" todir="${build.classes.dir}" />
</target>
+ <target name="-post-jar">
+ <!-- jars -->
+ <delete file="${dist.dir}/jars/lib/jEdit.jar" />
+ <move todir="${dist.dir}/jars">
+ <fileset dir="${dist.dir}/jars/lib" />
+ </move>
+ <copy file="${scala.library}" todir="${dist.dir}/jars" />
+ <!-- clean up -->
+ <delete dir="{dist.dir}/jars/lib" />
+ <!-- dist-template -->
+ <copy file="dist-template/properties/jedit.props" tofile="${dist.dir}/properties" />
+ <copy todir="${dist.dir}/modes">
+ <fileset dir="dist-template/modes">
+ <exclude name="catalog-template" />
+ </fileset>
+ </copy>
+ <copy file="dist-template/modes/catalog-template" tofile="${dist.dir}/modes/catalog" />
+ </target>
</project>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/modes/catalog-template Mon Mar 02 19:27:06 2009 +0100
@@ -0,0 +1,10 @@
+<?xml version="1.0"?>
+<!DOCTYPE MODES SYSTEM "catalog.dtd">
+
+<MODES>
+
+<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy" />
+<MODE NAME="ml" FILE="ml.xml" FILE_NAME_GLOB="*.ML" />
+
+</MODES>
+
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Mon Mar 02 19:27:06 2009 +0100
@@ -7,6 +7,8 @@
buffer.noTabs=true
buffer.tabSize=2
fallbackEncodings=US-ASCII ISO-8859-15
+firstTime=false
+tip.show=false
encodingDetectors=BOM XML-PI buffer-local-property
delete-line.shortcut=A+d
delete.shortcut2=C+d
--- a/src/Tools/jEdit/makedist Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/makedist Mon Mar 02 19:27:06 2009 +0100
@@ -12,7 +12,6 @@
## diagnostics
JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16"
-SCALA_HOME="/home/scala/current"
function usage()
{
@@ -22,8 +21,6 @@
echo " Options are:"
echo " -j DIR specify original jEdit distribution"
echo " (default: $JEDIT_HOME)"
- echo " -s DIR specify Scala distribution"
- echo " (default: $SCALA_HOME)"
echo
echo " Produce Isabelle/jEdit distribution from Netbeans build"
echo " in $THIS/dist"
@@ -48,9 +45,6 @@
j)
JEDIT_HOME="$OPTARG"
;;
- s)
- SCALA_HOME="$OPTARG"
- ;;
\?)
usage
;;
@@ -86,10 +80,7 @@
cp -R "$JEDIT_HOME/." "$JEDIT/."
rm -rf "$JEDIT/jEdit" "$JEDIT/build-support"
-mkdir -p "$JEDIT/jars"
-
-[ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME"
-cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"
+cp -R jars "$JEDIT/jars"
cp -R "$THIS/dist-template/." "$JEDIT/."
@@ -97,13 +88,6 @@
print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; }
print; }' "$JEDIT/modes/catalog"
-cp jars/Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar"
-cp jars/lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar"
-cp jars/lib/core-renderer.jar "$JEDIT/jars/"
-cp jars/lib/ErrorList.jar "$JEDIT/jars/"
-cp jars/lib/SideKick.jar "$JEDIT/jars/"
-
-
# build archive
echo "${JEDIT}.tar.gz"
--- a/src/Tools/jEdit/plugin/Isabelle.props Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props Mon Mar 02 19:27:06 2009 +0100
@@ -7,9 +7,9 @@
plugin.isabelle.jedit.Plugin.description=Isabelle/Isar live document editing
#system parameters
-plugin.isabelle.jedit.Plugin.activate=defer
+plugin.isabelle.jedit.Plugin.activate=startup
plugin.isabelle.jedit.Plugin.usePluginHome=false
-plugin.isabelle.jedit.Plugin.jars=isabelle-Pure.jar core-renderer.jar scala-library.jar
+plugin.isabelle.jedit.Plugin.jars=Pure.jar core-renderer.jar scala-library.jar
#dependencies
plugin.isabelle.jedit.Plugin.depend.0=jdk 1.5
@@ -23,7 +23,7 @@
options.isabelle.code=new isabelle.jedit.OptionPane();
options.isabelle.font-path.title=Font Path
options.isabelle.font-size.title=Font Size
-options.isabelle.font-size=14
+options.isabelle.font-size=18
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Mon Mar 02 19:27:06 2009 +0100
@@ -1,50 +1,121 @@
/*
* include isabelle's command- and keyword-declarations
* live in jEdits syntax-highlighting
- *
- * one TokenMarker per prover
*
* @author Fabian Immler, TU Munich
*/
package isabelle.jedit
-import org.gjt.sp.jedit.syntax.{ModeProvider, Token, TokenMarker, ParserRuleSet, KeywordMap}
+import isabelle.proofdocument.ProofDocument
+import isabelle.prover.{Command, MarkupNode}
+import isabelle.Markup
-class DynamicTokenMarker extends TokenMarker {
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.syntax._
- val ruleset = new ParserRuleSet("isabelle", "MAIN")
+import java.awt.Color
+import java.awt.Font
+import javax.swing.text.Segment;
+
+object DynamicTokenMarker {
- // copy rules and keywords from basic isabelle mode
- val original = ModeProvider.instance.getMode("isabelle").getTokenMarker.getMainRuleSet
- ruleset.addRuleSet(original)
- ruleset.setKeywords(new KeywordMap(false))
- ruleset.setDefault(0)
- ruleset.setDigitRegexp(null)
- ruleset.setEscapeRule(original.getEscapeRule)
- ruleset.setHighlightDigits(false)
- ruleset.setIgnoreCase(false)
- ruleset.setNoWordSep("_'.?")
- ruleset.setProperties(null)
- ruleset.setTerminateChar(-1)
-
- addRuleSet(ruleset)
+ def styles: Array[SyntaxStyle] = {
+ val array = new Array[SyntaxStyle](256)
+ // array(0) won't be used: reserved for global default-font
+ array(1) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
+ array(2) = new SyntaxStyle(new Color(255, 0, 255), Color.white, Isabelle.plugin.font)
+ array(3) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font)
+ array(4) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font)
+ array(5) = new SyntaxStyle(new Color(255, 128, 128), Color.white,Isabelle.plugin.font)
+ array(6) = new SyntaxStyle(Color.yellow, Color.white, Isabelle.plugin.font)
+ array(7) = new SyntaxStyle( new Color(0, 192, 0), Color.white, Isabelle.plugin.font)
+ array(8) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font)
+ array(9) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font)
+ array(10) = new SyntaxStyle(Color.gray, Color.white, Isabelle.plugin.font)
+ array(11) = new SyntaxStyle(Color.white, Color.white, Isabelle.plugin.font)
+ array(12) = new SyntaxStyle(Color.red, Color.white, Isabelle.plugin.font)
+ array(13) = new SyntaxStyle(Color.orange, Color.white, Isabelle.plugin.font)
+ return array
+ }
- private val kinds = List(
- OuterKeyword.minor -> Token.KEYWORD4,
- OuterKeyword.control -> Token.INVALID,
- OuterKeyword.diag -> Token.LABEL,
- OuterKeyword.heading -> Token.KEYWORD1,
- OuterKeyword.theory1 -> Token.KEYWORD4,
- OuterKeyword.theory2 -> Token.KEYWORD1,
- OuterKeyword.proof1 -> Token.KEYWORD1,
- OuterKeyword.proof2 -> Token.KEYWORD2,
- OuterKeyword.improper -> Token.DIGIT
- )
- def += (name: String, kind: String) = {
- kinds.find(pair => pair._1.contains(kind)) match {
- case None =>
- case Some((_, kind_byte)) => getMainRuleSet.getKeywords.add(name, kind_byte)
+ def choose_byte(kind: String): Byte = {
+ // TODO: as properties
+ kind match {
+ // logical entities
+ case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
+ | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
+ | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => 2
+ // inner syntax
+ case Markup.TFREE | Markup.FREE => 3
+ case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => 4
+ case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
+ | Markup.INNER_COMMENT => 5
+ case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
+ | Markup.ATTRIBUTE | Markup.METHOD => 6
+ // embedded source text
+ case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
+ | Markup.DOC_ANTIQ => 7
+ // outer syntax
+ case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => 8
+ case Markup.VERBATIM => 9
+ case Markup.COMMENT => 10
+ case Markup.CONTROL => 11
+ case Markup.MALFORMED => 12
+ case Markup.STRING | Markup.ALTSTRING => 13
+ // other
+ case _ => 1
}
}
+
+ def choose_color(kind : String) : Color = styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor
+
}
+
+class DynamicTokenMarker(buffer: JEditBuffer, document: ProofDocument) extends TokenMarker {
+
+ override def markTokens(prev: TokenMarker.LineContext,
+ handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = {
+ val previous = prev.asInstanceOf[IndexLineContext]
+ val line = if(prev == null) 0 else previous.line + 1
+ val context = new IndexLineContext(line, previous)
+ val start = buffer.getLineStartOffset(line)
+ val stop = start + line_segment.count
+
+ def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
+ def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
+
+ val commands = document.commands.dropWhile(_.stop <= from(start))
+ if(commands.hasNext) {
+ var next_x = start
+ for {
+ command <- commands.takeWhile(_.start < from(stop))
+ markup <- command.root_node.flatten
+ if(to(markup.abs_stop) > start)
+ if(to(markup.abs_start) < stop)
+ byte = DynamicTokenMarker.choose_byte(markup.kind)
+ token_start = to(markup.abs_start) - start max 0
+ token_length = to(markup.abs_stop) - to(markup.abs_start) -
+ (start - to(markup.abs_start) max 0) -
+ (to(markup.abs_stop) - stop max 0)
+ } {
+ if (start + token_start > next_x)
+ handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
+ handler.handleToken(line_segment, byte, token_start, token_length, context)
+ next_x = start + token_start + token_length
+ }
+ if (next_x < stop)
+ handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
+ } else {
+ handler.handleToken(line_segment, 1, 0, line_segment.count, context)
+ }
+
+ handler.handleToken(line_segment,Token.END, line_segment.count, 0, context)
+ handler.setLineContext(context)
+ return context
+ }
+
+}
+
+class IndexLineContext(val line: Int, prev: IndexLineContext)
+ extends TokenMarker.LineContext(new ParserRuleSet("isabelle", "MAIN"), prev)
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Mar 02 19:27:06 2009 +0100
@@ -17,7 +17,7 @@
import org.gjt.sp.jedit.buffer.JEditBuffer;
import org.gjt.sp.jedit._
-class PhaseOverviewPanel(prover : isabelle.prover.Prover) extends JPanel(new BorderLayout) {
+class PhaseOverviewPanel(prover: isabelle.prover.Prover, to_current: Int => Int) extends JPanel(new BorderLayout) {
private val WIDTH = 10
private val HILITE_HEIGHT = 2
@@ -25,7 +25,7 @@
val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
prover.command_info += (_ => repaint_delay.delay_or_ignore())
-
+
setRequestFocusEnabled(false);
addMouseListener(new MouseAdapter {
@@ -59,8 +59,8 @@
}
private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
- val line1 = buffer.getLineOfOffset(command.start)
- val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
+ val line1 = buffer.getLineOfOffset(to_current(command.start))
+ val line2 = buffer.getLineOfOffset(to_current(command.stop - 1)) + 1
val y = lineToY(line1)
val height = lineToY(line2) - y - 1
val (light, dark) = command.status match {
@@ -84,7 +84,7 @@
val buffer = textarea.getBuffer
for (c <- prover.document.commands)
paintCommand(c, buffer, gfx)
-
+
}
override def getPreferredSize : Dimension =
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Mar 02 19:27:06 2009 +0100
@@ -35,7 +35,7 @@
def activate(view: View) {
prover = new Prover(Isabelle.system, Isabelle.default_logic)
-
+
val buffer = view.getBuffer
val path = buffer.getPath
@@ -73,13 +73,6 @@
state_panel.setDocument(state.result_document, UserAgent.baseURL)
}
})
-
- // one independent token marker per prover
- val token_marker = new DynamicTokenMarker
- buffer.setTokenMarker(token_marker)
-
- // register for new declarations
- prover.decl_info += (pair => token_marker += (pair._1, pair._2))
}
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Mar 02 19:27:06 2009 +0100
@@ -35,35 +35,6 @@
case _ => Color.red
}
}
-
- def choose_color(markup: String): Color = {
- // TODO: as properties
- markup match {
- // logical entities
- case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
- | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
- | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => new Color(255, 0, 255)
- // inner syntax
- case Markup.TFREE | Markup.FREE => Color.blue
- case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Color.green
- case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
- | Markup.INNER_COMMENT => new Color(255, 128, 128)
- case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
- | Markup.ATTRIBUTE | Markup.METHOD => Color.yellow
- // embedded source text
- case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
- | Markup.DOC_ANTIQ => new Color(0, 192, 0)
- // outer syntax
- case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => Color.blue
- case Markup.VERBATIM => Color.green
- case Markup.COMMENT => Color.gray
- case Markup.CONTROL => Color.white
- case Markup.MALFORMED => Color.red
- case Markup.STRING | Markup.ALTSTRING => Color.orange
- // other
- case _ => Color.white
- }
- }
}
@@ -78,29 +49,25 @@
private var col: Text.Changed = null
private val col_timer = new Timer(300, new ActionListener() {
- override def actionPerformed(e: ActionEvent) = commit()
+ override def actionPerformed(e: ActionEvent) = commit
})
col_timer.stop
col_timer.setRepeats(true)
- private val phase_overview = new PhaseOverviewPanel(prover)
+ private val phase_overview = new PhaseOverviewPanel(prover, to_current(_))
/* activation */
- Isabelle.plugin.font_changed += (_ => update_font())
+ Isabelle.plugin.font_changed += (_ => update_styles)
- private def update_font() = {
+ private def update_styles = {
if (text_area != null) {
if (Isabelle.plugin.font != null) {
- val painter = text_area.getPainter
- painter.setStyles(painter.getStyles.map(style =>
- new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, Isabelle.plugin.font)
- ))
- painter.setFont(Isabelle.plugin.font)
- repaint_all()
+ text_area.getPainter.setStyles(DynamicTokenMarker.styles)
+ repaint_all
}
}
}
@@ -119,7 +86,8 @@
phase_overview.textarea = text_area
text_area.addLeftOfScrollBar(phase_overview)
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
- update_font()
+ buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
+ update_styles
}
def deactivate() = {
@@ -134,13 +102,13 @@
val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
prover.command_info += (_ => repaint_delay.delay_or_ignore())
- private def from_current(pos: Int) =
+ def from_current (pos: Int) =
if (col != null && col.start <= pos)
if (pos < col.start + col.added) col.start
else pos - col.added + col.removed
else pos
- private def to_current(pos : Int) =
+ def to_current (pos : Int) =
if (col != null && col.start <= pos)
if (pos < col.start + col.removed) col.start
else pos + col.added - col.removed
@@ -172,7 +140,8 @@
if (finish < buffer.getLength) text_area.offsetToXY(finish)
else {
val p = text_area.offsetToXY(finish - 1)
- p.x = p.x + text_area.getPainter.getFontMetrics.charWidth(' ')
+ val metrics = text_area.getPainter.getFontMetrics
+ p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
p
}
@@ -203,10 +172,10 @@
// paint details of command
for (node <- e.root_node.dfs) {
val begin = to_current(node.start + e.start)
- val finish = to_current(node.end + e.start)
+ val finish = to_current(node.stop + e.start)
if (finish > start && begin < end) {
- encolor(gfx, y + metrics.getHeight - 4, 2, begin max start, finish min end,
- TheoryView.choose_color(node.short), true)
+ encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1,
+ DynamicTokenMarker.choose_color(node.kind), true)
}
}
e = e.next
@@ -225,7 +194,7 @@
/* BufferListener methods */
- private def commit() {
+ private def commit {
if (col != null)
changes.event(col)
col = null
@@ -233,7 +202,7 @@
col_timer.stop()
}
- private def delay_commit() {
+ private def delay_commit {
if (col_timer.isRunning())
col_timer.restart()
else
@@ -250,10 +219,10 @@
else if (col.start <= offset && offset <= col.start + col.added)
col = new Text.Changed(col.start, col.added + length, col.removed)
else {
- commit()
+ commit
col = new Text.Changed(offset, length, 0)
}
- delay_commit()
+ delay_commit
*/
changes.event(new Text.Changed(offset, length, 0))
}
@@ -265,7 +234,7 @@
if (col == null)
col = new Text.Changed(start, 0, removed)
else if (col.start > start + removed || start > col.start + col.added) {
- commit()
+ commit
col = new Text.Changed(start, 0, removed)
}
else {
@@ -278,7 +247,7 @@
(diff - (offset min 0), offset min 0)
col = new Text.Changed(start min col.start, added, col.removed - add_removed)
}
- delay_commit()
+ delay_commit
*/
changes.event(new Text.Changed(start, 0, removed))
}
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Mar 02 19:27:06 2009 +0100
@@ -230,11 +230,13 @@
val structural_changes = new EventBus[StructureChange]
- def commands = new Iterator[Command] {
- var current = first_token
+ def commands_from(start: Token) = new Iterator[Command] {
+ var current = start
def hasNext = current != null
- def next() = { val s = current.command ; current = s.last.next ; s }
+ def next = { val s = current.command ; current = s.last.next ; s }
}
+ def commands_from(start: Command): Iterator[Command] = commands_from(start.first)
+ def commands = commands_from(first_token)
def find_command_at(pos: Int): Command = {
for (cmd <- commands) { if (pos < cmd.stop) return cmd }
--- a/src/Tools/jEdit/src/prover/Command.scala Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Mon Mar 02 19:27:06 2009 +0100
@@ -104,7 +104,7 @@
new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
def node_from(kind: String, begin: Int, end: Int) = {
- val markup_content = /*content.substring(begin, end)*/ ""
+ val markup_content = content.substring(begin, end)
new MarkupNode(this, begin, end, id, kind, markup_content)
}
}
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Mar 02 19:27:06 2009 +0100
@@ -20,29 +20,33 @@
object RelativeAsset extends IAsset {
override def getIcon : Icon = null
- override def getShortString : String = node.short
- override def getLongString : String = node.long
- override def getName : String = node.name
- override def setName(name : String) = ()
+ override def getShortString : String = node.kind
+ override def getLongString : String = node.desc
+ override def getName : String = node.id
+ override def setName (name : String) = ()
override def setStart(start : Position) = ()
- override def getStart : Position = node.base.start + node.start
+ override def getStart : Position = node.abs_start
override def setEnd(end : Position) = ()
- override def getEnd : Position = node.base.start + node.end
- override def toString = node.name + ": " + node.short
+ override def getEnd : Position = node.abs_stop
+ override def toString = node.id + ": " + node.kind + "[" + node.start + " - " + node.stop + "]"
}
new DefaultMutableTreeNode(RelativeAsset)
}
}
-class MarkupNode (val base : Command, val start : Int, val end : Int,
- val name : String, val short : String, val long : String) {
+class MarkupNode (val base : Command, val start : Int, val stop : Int,
+ val id : String, val kind : String, val desc : String) {
val swing_node : DefaultMutableTreeNode = MarkupNode.markup2default_node (this)
var parent : MarkupNode = null
def orphan = parent == null
+ def length = stop - start
+ def abs_start = base.start + start
+ def abs_stop = base.start + stop
+
private var children_cell : List[MarkupNode] = Nil
//track changes in swing_node
def children = children_cell
@@ -51,10 +55,10 @@
for (c <- cs) swing_node add c.swing_node
children_cell = cs
}
-
+
private def add(child : MarkupNode) {
child parent = this
- children_cell = (child :: children) sort ((a, b) => a.start < b.end)
+ children_cell = (child :: children) sort ((a, b) => a.start < b.start)
swing_node add child.swing_node
}
@@ -78,6 +82,28 @@
all
}
+ def leafs: List[MarkupNode] = {
+ if (children == Nil) return List(this)
+ else return children flatMap (_.leafs)
+ }
+
+ def flatten: List[MarkupNode] = {
+ var next_x = start
+ if(children.length == 0) List(this)
+ else {
+ val filled_gaps = for {
+ child <- children
+ markups = if (next_x < child.start) {
+ new MarkupNode(base, next_x, child.start, id, kind, "") :: child.flatten
+ } else child.flatten
+ update = (next_x = child.stop)
+ markup <- markups
+ } yield markup
+ if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, kind, "")
+ else filled_gaps
+ }
+ }
+
def insert(new_child : MarkupNode) : Unit = {
if (new_child fitting_into this) {
for (child <- children) {
@@ -96,13 +122,14 @@
this remove new_child.children
}
} else {
- System.err.println("ignored nonfitting markup " + new_child.name + new_child.short + new_child.long
- + "(" +new_child.start + ", "+ new_child.end + ")")
+ System.err.println("ignored nonfitting markup " + new_child.id + new_child.kind + new_child.desc
+ + "(" +new_child.start + ", "+ new_child.stop + ")")
}
}
// does this fit into node?
def fitting_into(node : MarkupNode) = node.start <= this.start &&
- node.end >= this.end
-
+ node.stop >= this.stop
+
+ override def toString = "([" + start + " - " + stop + "] " + id + "( " + kind + "): " + desc
}