--- a/src/Tools/jEdit/src/prover/Command.scala Tue Jan 27 18:15:11 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Tue Jan 27 18:16:24 2009 +0100
@@ -34,7 +34,10 @@
class Command(text: Text, val first: Token, val last: Token)
{
val id = Isabelle.plugin.id()
-
+
+
+ /* content */
+
{
var t = first
while (t != null) {
@@ -43,37 +46,6 @@
}
}
-
- /* command status */
-
- private var _status = Command.Status.UNPROCESSED
- def status = _status
- def status_=(st: Command.Status.Value) = {
- if (st == Command.Status.UNPROCESSED) {
- // delete markup
- for (child <- root_node.children) {
- child.children = Nil
- }
- }
- _status = st
- }
-
-
- /* accumulated results */
-
- private val results = new mutable.ListBuffer[XML.Tree]
- def add_result(tree: XML.Tree) { results += tree }
-
- def result_document = XML.document(
- results.toList match {
- case Nil => XML.Elem("message", Nil, Nil)
- case List(elem) => elem
- case elems => XML.Elem("messages", Nil, List(elems.first, elems.last)) // FIXME all elems!?
- }, "style")
-
-
- /* content */
-
override def toString = name
val name = text.content(first.start, first.stop)
@@ -94,7 +66,38 @@
}
- /* markup tree */
+ /* command status */
+
+ private var _status = Command.Status.UNPROCESSED
+ def status = _status
+ def status_=(st: Command.Status.Value) {
+ if (st == Command.Status.UNPROCESSED) {
+ // delete markup
+ for (child <- root_node.children) {
+ child.children = Nil
+ }
+ }
+ _status = st
+ }
+
+
+ /* results */
+
+ private val results = new mutable.ListBuffer[XML.Tree]
+ def add_result(tree: XML.Tree) { results += tree }
+
+ private val state_results = new mutable.ListBuffer[XML.Tree]
+ def add_state_result(tree: XML.Tree) { state_results += tree }
+
+ def result_document = XML.document(
+ results.toList ::: state_results.toList match {
+ case Nil => XML.Elem("message", Nil, Nil)
+ case List(elem) => elem
+ case elems => XML.Elem("messages", Nil, elems)
+ }, "style")
+
+
+ /* markup */
val root_node =
new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)