# HG changeset patch # User immler@in.tum.de # Date 1240833785 -7200 # Node ID 7c001369956abb9e2c02c09044442fa3cb77fb0d # Parent 7dc6c231da4065fc08f4c5197ef7e164f8d8da56 included information on ML status messages in Sidekick's status-window diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Apr 22 17:35:49 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Mon Apr 27 14:03:05 2009 +0200 @@ -85,7 +85,7 @@ markup <- command.root_node.flatten if(to(markup.abs_stop(document)) > start) if(to(markup.abs_start(document)) < stop) - byte = DynamicTokenMarker.choose_byte(markup.kind) + byte = DynamicTokenMarker.choose_byte(markup.desc) 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 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Apr 22 17:35:49 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Apr 27 14:03:05 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.kind, text_area.getPainter.getStyles), true) + DynamicTokenMarker.choose_color(node.desc, text_area.getPainter.getStyles), true) } } } diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Wed Apr 22 17:35:49 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Command.scala Mon Apr 27 14:03:05 2009 +0200 @@ -82,12 +82,12 @@ val root_node = new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, Markup.COMMAND_SPAN, content) - def add_markup(kind: String, begin: Int, end: Int) = { + 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, kind, markup_content) + root_node insert new MarkupNode(this, begin, end, id, markup_content, desc) } } diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/prover/MarkupNode.scala --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Wed Apr 22 17:35:49 2009 +0200 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Apr 27 14:03:05 2009 +0200 @@ -22,7 +22,7 @@ object RelativeAsset extends IAsset { override def getIcon : Icon = null - override def getShortString : String = node.kind + override def getShortString : String = node.content override def getLongString : String = node.desc override def getName : String = node.id override def setName (name : String) = () @@ -30,7 +30,7 @@ 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.kind + "[" + getStart + " - " + getEnd + "]" + override def toString = node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]" } new DefaultMutableTreeNode(RelativeAsset) @@ -38,7 +38,7 @@ } class MarkupNode (val base : Command, val start : Int, val stop : Int, - val id : String, val kind : String, val desc : String) { + val id : String, val content : String, val desc : String) { def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = { val node = MarkupNode.markup2default_node (this, base, doc) @@ -83,12 +83,12 @@ val filled_gaps = for { child <- children markups = if (next_x < child.start) { - new MarkupNode(base, next_x, child.start, id, kind, "") :: child.flatten + new MarkupNode(base, next_x, child.start, 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, kind, "") + if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, content, "") else filled_gaps } } @@ -111,7 +111,7 @@ this remove new_child.children } } else { - System.err.println("ignored nonfitting markup " + new_child.id + new_child.kind + new_child.desc + System.err.println("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc + "(" +new_child.start + ", "+ new_child.stop + ")") } } @@ -120,5 +120,5 @@ def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop - override def toString = "([" + start + " - " + stop + "] " + id + "( " + kind + "): " + desc + override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + desc } diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Wed Apr 22 17:35:49 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Prover.scala Mon Apr 27 14:03:05 2009 +0200 @@ -98,6 +98,10 @@ private def handle_result(result: IsabelleProcess.Result) { + // helper-function (move to XML?) + def get_attr(attributes: List[(String, String)], attr: String): Option[String] = + attributes.find(kv => kv._1 == attr).map(_._2) + def command_change(c: Command) = this ! c val (running, command) = result.props.find(p => p._1 == Markup.ID) match { @@ -176,13 +180,26 @@ 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) => + 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) + command_change(command) // other markup - case XML.Elem(kind, - (Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) :: - (Markup.ID, markup_id) :: _, _) => - val begin = offset.toInt - 1 - val end = end_offset.toInt - 1 + 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