immutable markup-nodes;
more seperate nodes in command;
restructured handling of markups in prover
--- a/src/Tools/jEdit/src/prover/Command.scala Mon Apr 27 17:33:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Wed Apr 29 16:08:22 2009 +0200
@@ -53,9 +53,10 @@
if (st == Command.Status.UNPROCESSED) {
state_results.clear
// delete markup
- for (child <- root_node.children) {
- child.children = Nil
- }
+ state_markup = empty_root_node
+ highlight_markup = empty_root_node
+ types_markup = empty_root_node
+ refs_markup = empty_root_node
}
_status = st
}
@@ -79,23 +80,24 @@
/* markup */
- val root_node =
- new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, content, Markup.COMMAND_SPAN)
+ val empty_root_node =
+ new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil, id, content, Markup.COMMAND_SPAN)
+
+ var command_markup = empty_root_node
- def add_markup(desc: String, begin: Int, end: Int) = {
- val markup_content = if (end <= content.length) content.substring(begin, end)
- else {
- System.err.println (root_node.stop, content, content.length, end)
- "wrong indices?"
- }
- root_node insert new MarkupNode(this, begin, end, id, markup_content, desc)
- }
+ var state_markup = empty_root_node
+ var highlight_markup = empty_root_node
+ var types_markup = empty_root_node
+ var refs_markup = empty_root_node
+ var state_markups = List(state_markup, highlight_markup, types_markup, refs_markup)
- // syntax highlighting
- val highlight_node =
- new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, content, Markup.COMMAND_SPAN)
+ def highlight_node = (command_markup /: highlight_markup.children) (_ + _)
+
+ def root_node = (command_markup /: state_markup.children) (_ + _)
- def add_highlight(kind: String, begin: Int, end: Int) =
- highlight_node insert new MarkupNode(this, begin, end, id, "", kind)
+ def markup_node(desc: String, begin: Int, end: Int) =
+ new MarkupNode(this, begin, end, Nil, id,
+ if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??",
+ desc)
}
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Apr 27 17:33:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Wed Apr 29 16:08:22 2009 +0200
@@ -38,30 +38,24 @@
}
class MarkupNode (val base : Command, val start : Int, val stop : Int,
- val id : String, val content : String, val desc : String) {
+ val children: List[MarkupNode],
+ val id : String, val content : String, val desc : String) {
def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
val node = MarkupNode.markup2default_node (this, base, doc)
- for (c <- children) node add c.swing_node(doc)
+ children.map(node add _.swing_node(doc))
node
}
-
+
def abs_start(doc: ProofDocument) = base.start(doc) + start
def abs_stop(doc: ProofDocument) = base.start(doc) + stop
- var parent : MarkupNode = null
- def orphan = parent == null
-
- var children : List[MarkupNode] = Nil
+ def set_children(newchildren: List[MarkupNode]): MarkupNode =
+ new MarkupNode(base, start, stop, newchildren, id, content, desc)
- private def add(child : MarkupNode) {
- child parent = this
- 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))
- private def remove(nodes : List[MarkupNode]) {
- children = children diff nodes
- }
+ def remove(nodes : List[MarkupNode]) = set_children(children diff nodes)
def dfs : List[MarkupNode] = {
var all = Nil : List[MarkupNode]
@@ -83,42 +77,33 @@
val filled_gaps = for {
child <- children
markups = if (next_x < child.start) {
- new MarkupNode(base, next_x, child.start, id, content, "") :: child.flatten
+ new MarkupNode(base, next_x, child.start, Nil, id, content, "") :: 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, content, "")
+ if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, "")
else filled_gaps
}
}
- def insert(new_child : MarkupNode) : Unit = {
+ def +(new_child : MarkupNode) : MarkupNode = {
if (new_child fitting_into this) {
- for (child <- children) {
- if (new_child fitting_into child)
- child insert new_child
+ val new_children = children.map(c => if((new_child fitting_into c)) c + new_child else c)
+ if (new_children == children) {
+ // new_child did not fit into children of this -> insert new_child between this and its children
+ val (fitting, nonfitting) = children span(_ fitting_into new_child)
+ this remove fitting add ((new_child /: fitting) (_ add _))
}
- if (new_child orphan) {
- // new_child did not fit into children of this
- // -> insert new_child between this and its children
- for (child <- children) {
- if (child fitting_into new_child) {
- new_child add child
- }
- }
- this add new_child
- this remove new_child.children
- }
+ else this set_children new_children
} else {
- System.err.println("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc
+ error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc
+ "(" +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 + "): " + desc
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Mon Apr 27 17:33:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Wed Apr 29 16:08:22 2009 +0200
@@ -180,37 +180,29 @@
output_info.event(result.toString)
command.status = Command.Status.FAILED
command_change(command)
- // ML typing
- case XML.Elem(Markup.ML_TYPING, attr, body) =>
- val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
- val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
- val markup_id = get_attr(attr, Markup.ID).get
- val info = body.first.asInstanceOf[XML.Text].content
- command.add_markup(info, begin, end)
- command_change(command)
- // ML references
- case XML.Elem(Markup.ML_REF, attr, body) =>
+ case XML.Elem(kind, attr, body) =>
+ // TODO: assuming that begin, end, id are present in attributes
val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
val markup_id = get_attr(attr, Markup.ID).get
- command.add_markup(body.toString, begin, end)
+ kind match {
+ case Markup.ML_TYPING =>
+ val info = body.first.asInstanceOf[XML.Text].content
+ command.types_markup += command.markup_node(info, begin, end)
+ command.state_markup += command.markup_node(info, begin, end)
+ case Markup.ML_REF =>
+ command.refs_markup += command.markup_node(body.toString, begin, end)
+ command.state_markup += command.markup_node(body.toString, begin, end)
+ case kind =>
+ if (!running)
+ commands.get(markup_id).map (cmd =>
+ cmd.command_markup += cmd.markup_node(kind, begin, end))
+ else {
+ command.highlight_markup += command.markup_node(kind, begin, end)
+ command.state_markup += command.markup_node(kind, begin, end)
+ }
+ }
command_change(command)
- // syntax highlighting
- case XML.Elem(kind, attr, body) =>
- val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
- val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
- val markup_id = get_attr(attr, Markup.ID).get
-
- val cmd = // FIXME proper command version!? running!?
- // outer syntax: no id in props
- if (command == null) commands.getOrElse(markup_id, null)
- // inner syntax: id from props
- else command
- if (cmd != null) {
- cmd.add_markup(kind, begin, end)
- cmd.add_highlight(kind, begin, end)
- command_change(cmd)
- }
case _ =>
//}}}
}