--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Fri May 22 13:43:34 2009 +0200
@@ -33,7 +33,7 @@
if (prover_setup.isDefined) {
val document = prover_setup.get.prover.document
for (command <- document.commands)
- data.root.add(command.root_node.swing_node(document))
+ data.root.add(command.highlight_node.swing_node(document))
if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
} else {
--- a/src/Tools/jEdit/src/prover/Command.scala Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Fri May 22 13:43:34 2009 +0200
@@ -53,10 +53,10 @@
if (st == Command.Status.UNPROCESSED) {
state_results.clear
// delete markup
- state_markup = empty_root_node
- highlight_markup = empty_root_node
- types_markup = empty_root_node
- refs_markup = empty_root_node
+ markup_root.filter(_.kind match {
+ case MarkupNode.RootNode() | MarkupNode.OuterNode() => true
+ case _ => false
+ })
}
_status = st
}
@@ -81,23 +81,22 @@
/* markup */
val empty_root_node =
- new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil, id, content, Markup.COMMAND_SPAN)
+ new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil,
+ id, content, Markup.COMMAND_SPAN, MarkupNode.RootNode())
- var command_markup = empty_root_node
+ var markup_root = empty_root_node
- 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)
+ def highlight_node: MarkupNode = {
+ import MarkupNode._
+ markup_root.filter(_.kind match {
+ case RootNode() | OuterNode() | HighlightNode() => true
+ case _ => false
+ }).head
+ }
- def highlight_node = (command_markup /: highlight_markup.children) (_ + _)
-
- def root_node = (command_markup /: state_markup.children) (_ + _)
-
- def markup_node(desc: String, begin: Int, end: Int) =
+ def markup_node(desc: String, begin: Int, end: Int, kind: MarkupNode.Kind) =
new MarkupNode(this, begin, end, Nil, id,
if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??",
- desc)
+ desc, kind)
}
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Fri May 22 13:43:34 2009 +0200
@@ -14,6 +14,12 @@
import javax.swing.tree._
object MarkupNode {
+ abstract class Kind
+ case class RootNode extends Kind
+ case class OuterNode extends Kind
+ case class HighlightNode extends Kind
+ case class TypeNode extends Kind
+ case class RefNode extends Kind
def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = {
@@ -37,9 +43,10 @@
}
}
-class MarkupNode (val base : Command, val start : Int, val stop : Int,
+class MarkupNode (val base: Command, val start: Int, val stop: Int,
val children: List[MarkupNode],
- val id : String, val content : String, val desc : String) {
+ val id: String, val content: String, val desc: String,
+ val kind: MarkupNode.Kind) {
def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
val node = MarkupNode.markup2default_node (this, base, doc)
@@ -51,7 +58,7 @@
def abs_stop(doc: ProofDocument) = base.start(doc) + stop
def set_children(newchildren: List[MarkupNode]): MarkupNode =
- new MarkupNode(base, start, stop, newchildren, id, content, desc)
+ new MarkupNode(base, start, stop, newchildren, id, content, desc, kind)
def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start))
@@ -77,12 +84,12 @@
val filled_gaps = for {
child <- children
markups = if (next_x < child.start) {
- new MarkupNode(base, next_x, child.start, Nil, id, content, desc) :: child.flatten
+ new MarkupNode(base, next_x, child.start, Nil, id, content, desc, 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, Nil, id, content, desc)
+ if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, desc, kind)
else filled_gaps
}
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Fri May 22 13:43:34 2009 +0200
@@ -188,18 +188,15 @@
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)
+ command.markup_root += command.markup_node(info, begin, end, MarkupNode.TypeNode())
case Markup.ML_REF =>
- command.refs_markup += command.markup_node(body.toString, begin, end)
- command.state_markup += command.markup_node(body.toString, begin, end)
+ command.markup_root += command.markup_node(body.toString, begin, end, MarkupNode.RefNode())
case kind =>
if (!running)
commands.get(markup_id).map (cmd =>
- cmd.command_markup += cmd.markup_node(kind, begin, end))
+ cmd.markup_root += cmd.markup_node(kind, begin, end, MarkupNode.OuterNode()))
else {
- command.highlight_markup += command.markup_node(kind, begin, end)
- command.state_markup += command.markup_node(kind, begin, end)
+ command.markup_root += command.markup_node(kind, begin, end, MarkupNode.HighlightNode())
}
}
command_change(command)