--- 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) -
--- 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)
}
}
}
--- 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)
}
}
--- 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
}
--- 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