# HG changeset patch # User immler@in.tum.de # Date 1242992615 -7200 # Node ID 850dc36d49264f034ff7781fdd6db19c99e94bc3 # Parent 0c1c8f8ee384607975e303e961da9040a00cef11 let MarkupNode carry arbitrary information diff -r 0c1c8f8ee384 -r 850dc36d4926 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Fri May 22 13:43:35 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Fri May 22 13:43:35 2009 +0200 @@ -85,7 +85,7 @@ markup <- command.highlight_node.flatten if(to(markup.abs_stop(document)) > start) if(to(markup.abs_start(document)) < stop) - byte = DynamicTokenMarker.choose_byte(markup.desc) + byte = DynamicTokenMarker.choose_byte(markup.info.toString) token_start = to(markup.abs_start(document)) - start max 0 token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) - (start - to(markup.abs_start(document)) max 0) - diff -r 0c1c8f8ee384 -r 850dc36d4926 src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Fri May 22 13:43:35 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Fri May 22 13:43:35 2009 +0200 @@ -204,7 +204,7 @@ val finish = to_current(node.abs_stop(document)) if (finish > start && begin < end) { encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1, - DynamicTokenMarker.choose_color(node.desc, text_area.getPainter.getStyles), true) + DynamicTokenMarker.choose_color(node.info.toString, text_area.getPainter.getStyles), true) } } } diff -r 0c1c8f8ee384 -r 850dc36d4926 src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Fri May 22 13:43:35 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Command.scala Fri May 22 13:43:35 2009 +0200 @@ -53,8 +53,8 @@ if (st == Command.Status.UNPROCESSED) { state_results.clear // delete markup - markup_root.filter(_.kind match { - case MarkupNode.RootNode() | MarkupNode.OuterNode() => true + markup_root.filter(_.info match { + case RootInfo() | OuterInfo(_) => true case _ => false }) } @@ -82,28 +82,28 @@ val empty_root_node = new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil, - id, content, Markup.COMMAND_SPAN, MarkupNode.RootNode()) + id, content, RootInfo()) var markup_root = empty_root_node def highlight_node: MarkupNode = { import MarkupNode._ - markup_root.filter(_.kind match { - case RootNode() | OuterNode() | HighlightNode() => true + markup_root.filter(_.info match { + case RootInfo() | OuterInfo(_) | HighlightInfo(_) => true case _ => false }).head } - def markup_node(desc: String, begin: Int, end: Int, kind: MarkupNode.Kind) = + def markup_node(begin: Int, end: Int, info: MarkupInfo) = new MarkupNode(this, begin, end, Nil, id, if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??", - desc, kind) + info) def type_at(pos: Int): String = { - val types = markup_root.filter(_.kind match {case MarkupNode.TypeNode() => true case _ => false}) + val types = markup_root.filter(_.info match {case TypeInfo(_) => true case _ => false}) types.flatten(_.flatten). find(t => t.start <= pos && t.stop > pos). - map(t => "\"" + t.content + "\" : " + t.desc). + map(t => "\"" + t.content + "\" : " + (t.info match {case TypeInfo(i) => i case _ => ""})). getOrElse(null) } } diff -r 0c1c8f8ee384 -r 850dc36d4926 src/Tools/jEdit/src/prover/MarkupNode.scala --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Fri May 22 13:43:35 2009 +0200 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Fri May 22 13:43:35 2009 +0200 @@ -13,13 +13,14 @@ import javax.swing.text.Position import javax.swing.tree._ +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 RefInfo(info: Any) extends MarkupInfo {override def toString = info.toString} + 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 = { @@ -29,7 +30,7 @@ object RelativeAsset extends IAsset { override def getIcon : Icon = null override def getShortString : String = node.content - override def getLongString : String = node.desc + override def getLongString : String = node.info.toString override def getName : String = node.id override def setName (name : String) = () override def setStart(start : Position) = () @@ -45,8 +46,7 @@ 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 kind: MarkupNode.Kind) { + val id: String, val content: String, val info: Any) { def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = { val node = MarkupNode.markup2default_node (this, base, doc) @@ -58,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, kind) + new MarkupNode(base, start, stop, newchildren, id, content, info) def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start)) @@ -84,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, kind) :: child.flatten + 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, desc, kind) + if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info) else filled_gaps } } @@ -111,7 +111,7 @@ } else this set_children new_children } else { - error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc + error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.info.toString + "(" +new_child.start + ", "+ new_child.stop + ")") } } @@ -119,5 +119,5 @@ // does this fit into node? def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop - override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + desc + override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString } diff -r 0c1c8f8ee384 -r 850dc36d4926 src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Fri May 22 13:43:35 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Prover.scala Fri May 22 13:43:35 2009 +0200 @@ -188,15 +188,15 @@ kind match { case Markup.ML_TYPING => val info = body.first.asInstanceOf[XML.Text].content - command.markup_root += command.markup_node(info, begin, end, MarkupNode.TypeNode()) + command.markup_root += command.markup_node(begin, end, TypeInfo(info)) case Markup.ML_REF => - command.markup_root += command.markup_node(body.toString, begin, end, MarkupNode.RefNode()) + command.markup_root += command.markup_node(begin, end, RefInfo(body)) case kind => if (!running) commands.get(markup_id).map (cmd => - cmd.markup_root += cmd.markup_node(kind, begin, end, MarkupNode.OuterNode())) + cmd.markup_root += cmd.markup_node(begin, end, OuterInfo(kind))) else { - command.markup_root += command.markup_node(kind, begin, end, MarkupNode.HighlightNode()) + command.markup_root += command.markup_node(begin, end, HighlightInfo(kind)) } } command_change(command)