src/Tools/jEdit/src/prover/Command.scala

--- a/src/Tools/jEdit/src/prover/Command.scala	Fri Nov 28 15:51:40 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Fri Nov 28 17:49:39 2008 +0100
@@ -36,12 +36,17 @@
   var phase = Phase.UNPROCESSED
 	
   var results = Nil : List[XML.Tree]
-  
+
+  //offsets relative to first.start!
+  class Status(val kind : String,val start : Int, val stop : Int ) { }
+  var statuses = Nil : List[Status]
+  def statusesxml = XML.Elem("statuses", List(), statuses.map (s => XML.Text(s.kind + ": " + s.start + "-" + s.stop + "\n")))
+
   def idString = java.lang.Long.toString(id, 36)
   def document = XML.document(results match {
                                 case Nil => XML.Elem("message", List(), List())
                                 case List(elem) => elem
-                                case _ => 
+                                case _ =>
                                   XML.Elem("messages", List(), List(results.first,
                                                                     results.last))
                               }, "style")
@@ -49,6 +54,22 @@
     results = results ::: List(tree)
   }
 
+  def addStatus(tree : XML.Tree) {
+    val (markup_info, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
+                                   case _ => null}
+
+    //process attributes:
+    var markup_begin = -1
+    var markup_end = -1
+    for((n, a) <- attr) {
+      if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - first.start
+      if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - first.start
+    }
+    if(markup_begin > -1 && markup_end > -1){
+          statuses = new Status(markup_info, markup_begin, markup_end) :: statuses
+    }
+  }
+
   def next = if (last.next != null) last.next.command else null
   def previous = if (first.previous != null) first.previous.command else null