--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 21:20:22 2009 +0200
@@ -15,31 +15,35 @@
abstract class MarkupInfo
case class RootInfo() extends MarkupInfo
-case class OuterInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
-case class HighlightInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
-case class TypeInfo(type_kind: String) extends MarkupInfo {override def toString = type_kind}
+case class OuterInfo(highlight: String) extends
+ MarkupInfo { override def toString = highlight }
+case class HighlightInfo(highlight: String) extends
+ MarkupInfo { override def toString = highlight }
+case class TypeInfo(type_kind: String) extends
+ MarkupInfo { override def toString = type_kind }
case class RefInfo(file: Option[String], line: Option[Int],
- command_id: Option[String], offset: Option[Int]) extends MarkupInfo {
- override def toString = (file, line, command_id, offset).toString
-}
+ command_id: Option[String], offset: Option[Int]) extends MarkupInfo {
+ override def toString = (file, line, command_id, offset).toString
+ }
object MarkupNode {
- def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = {
+ def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument)
+ : DefaultMutableTreeNode = {
implicit def int2pos(offset: Int): Position =
- new Position { def getOffset = offset; override def toString = offset.toString}
+ new Position { def getOffset = offset; override def toString = offset.toString }
object RelativeAsset extends IAsset {
- override def getIcon : Icon = null
- override def getShortString : String = node.content
- override def getLongString : String = node.info.toString
- override def getName : String = node.id
- override def setName (name : String) = ()
- override def setStart(start : Position) = ()
- override def getStart : Position = node.abs_start(doc)
- override def setEnd(end : Position) = ()
- override def getEnd : Position = node.abs_stop(doc)
+ override def getIcon: Icon = null
+ override def getShortString: String = node.content
+ override def getLongString: String = node.info.toString
+ override def getName: String = node.id
+ override def setName(name: String) = ()
+ override def setStart(start: Position) = ()
+ override def getStart: Position = node.abs_start(doc)
+ override def setEnd(end: Position) = ()
+ override def getEnd: Position = node.abs_stop(doc)
override def toString = node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
}
@@ -47,11 +51,11 @@
}
}
-class MarkupNode (val base: Command, val start: Int, val stop: Int,
- val children: List[MarkupNode],
- val id: String, val content: String, val info: MarkupInfo) {
-
- def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
+class MarkupNode(val base: Command, val start: Int, val stop: Int,
+ val children: List[MarkupNode],
+ val id: String, val content: String, val info: MarkupInfo)
+{
+ def swing_node(doc: ProofDocument): DefaultMutableTreeNode = {
val node = MarkupNode.markup2default_node (this, base, doc)
children.map(node add _.swing_node(doc))
node
@@ -63,11 +67,12 @@
def set_children(newchildren: List[MarkupNode]): MarkupNode =
new MarkupNode(base, start, stop, newchildren, id, content, info)
- def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start))
+ def add(child: MarkupNode) =
+ set_children ((child :: children) sort ((a, b) => a.start < b.start))
- def remove(nodes : List[MarkupNode]) = set_children(children diff nodes)
+ def remove(nodes: List[MarkupNode]) = set_children(children diff nodes)
- def dfs : List[MarkupNode] = {
+ def dfs: List[MarkupNode] = {
var all = Nil : List[MarkupNode]
for (child <- children)
all = child.dfs ::: all
@@ -86,41 +91,48 @@
else {
val filled_gaps = for {
child <- children
- markups = if (next_x < child.start) {
- new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten
- } else child.flatten
+ markups =
+ if (next_x < child.start) {
+ new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: 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, Nil, id, content, info)
+ if (next_x < stop)
+ filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info)
else filled_gaps
}
}
- def filter(p: (MarkupNode => Boolean)): List[MarkupNode] = {
+ def filter(p: MarkupNode => Boolean): List[MarkupNode] = {
val filtered = children.flatMap(_.filter(p))
if (p(this)) List(this set_children(filtered))
else filtered
}
- def +(new_child : MarkupNode) : MarkupNode = {
+ def +(new_child: MarkupNode): MarkupNode = {
if (new_child fitting_into this) {
var inserted = false
- val new_children = children.map(c => if((new_child fitting_into c) && !inserted) {inserted = true; c + new_child} else c)
+ val new_children =
+ children.map(c =>
+ if ((new_child fitting_into c) && !inserted) {inserted = true; c + new_child}
+ else c)
if (!inserted) {
- // new_child did not fit into children of this -> insert new_child between this and its children
+ // new_child did not fit into children of this
+ // -> insert new_child between this and its children
val fitting = children filter(_ fitting_into new_child)
(this remove fitting) add ((new_child /: fitting) (_ + _))
}
else this set_children new_children
} else {
- error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.info.toString
- + "(" +new_child.start + ", "+ new_child.stop + ")")
+ error("ignored nonfitting markup " + new_child.id + new_child.content +
+ new_child.info.toString + "(" +new_child.start + ", "+ new_child.stop + ")")
}
}
// does this fit into node?
- def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop
+ def fitting_into(node: MarkupNode) = node.start <= this.start && node.stop >= this.stop
- override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
+ override def toString =
+ "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
}