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

basic tree structure for sidekick

package isabelle.prover

import isabelle.proofdocument.Token
import isabelle.jedit.Plugin
import isabelle.{ YXML, XML }
import sidekick.{SideKickParsedData}
import sidekick.enhanced.SourceAsset
import javax.swing.text.Position
import javax.swing.tree.DefaultMutableTreeNode

object Command {
  object Phase extends Enumeration {
    val UNPROCESSED = Value("UNPROCESSED")
    val FINISHED = Value("FINISHED")
    val REMOVE = Value("REMOVE")
    val REMOVED = Value("REMOVED")
    val FAILED = Value("FAILED")
  }

  private var nextId : Long = 0
  def generateId : Long = {
    nextId = nextId + 1
    return nextId
  }
  
  def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
}

class Command(val first : Token[Command], val last : Token[Command]) {
  import Command._
  
  {
    var t = first
    while(t != null) {
      t.command = this
      t = if (t == last) null else t.next
    }
  }
  
  val id : Long = generateId
  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 _ =>
                                  XML.Elem("messages", List(), List(results.first,
                                                                    results.last))
                              }, "style")
  def addResult(tree : XML.Tree) {
    results = results ::: List(tree)
  }
  
  val root_node = {
    val content = Plugin.plugin.prover.document.getContent(this)
    val ra = new RelativeAsset(this, 0, stop - start, "command", content)
    System.err.println(start + "-" + stop + ": " + content)
    new DefaultMutableTreeNode(ra)
  }

  // does cand fit into node?
  private def fitting(cand : DefaultMutableTreeNode, node : DefaultMutableTreeNode) : boolean = {
    val node_asset = node.getUserObject.asInstanceOf[RelativeAsset]
    val n_start = node_asset.rel_start
    val n_end = node_asset.rel_end
    val cand_asset = cand.getUserObject.asInstanceOf[RelativeAsset]
    val c_start = cand_asset.rel_start
    val c_end = cand_asset.rel_end
    return c_start >= n_start && c_end <= n_end
  }

  def insert_node(new_node : DefaultMutableTreeNode, node : DefaultMutableTreeNode) {
    assert(fitting(new_node, node))
    val children = node.children
    while (children.hasMoreElements){
      val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode]
      if(fitting(new_node, child)) {
        insert_node(new_node, child)
      }
    }
    if(new_node.getParent == null){
      while(children.hasMoreElements){
        val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode]
        if(fitting(child, new_node)) {
          node.remove(child.asInstanceOf[DefaultMutableTreeNode])
          new_node.add(child)
        }
      }
      node.add(new_node)
    }
  }

 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
      val content = Plugin.plugin.prover.document.getContent(this).substring(markup_begin, markup_end)
      val asset = new RelativeAsset(this, markup_begin, markup_end, markup_info, content)
      val new_node = new DefaultMutableTreeNode(asset)
      insert_node(new_node, root_node)
    }
  }

  def next = if (last.next != null) last.next.command else null
  def previous = if (first.previous != null) first.previous.command else null

  def start = first start
  def stop = last stop
  
  def properStart = start
  def properStop = {
    var i = last
    while (i != first && i.kind.equals(Token.Kind.COMMENT))
      i = i.previous
    i.stop
  }  	
}