src/Tools/jEdit/src/prover/Command.scala
author immler@in.tum.de
Sun Dec 07 15:01:37 2008 +0100 (2008-12-07 ago)
changeset 34396 de809360c51d
parent 34394 7878d1100510
child 34397 86daaf5db016
permissions -rw-r--r--
command property: offset relative to start of command
wenzelm@34318
     1
package isabelle.prover
wenzelm@34318
     2
wenzelm@34318
     3
import isabelle.proofdocument.Token
immler@34393
     4
import isabelle.jedit.Plugin
wenzelm@34318
     5
import isabelle.{ YXML, XML }
immler@34393
     6
import sidekick.{SideKickParsedData}
immler@34393
     7
import sidekick.enhanced.SourceAsset
immler@34393
     8
import javax.swing.text.Position
immler@34393
     9
import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34318
    10
wenzelm@34318
    11
object Command {
wenzelm@34318
    12
  object Phase extends Enumeration {
wenzelm@34318
    13
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    14
    val FINISHED = Value("FINISHED")
wenzelm@34318
    15
    val REMOVE = Value("REMOVE")
wenzelm@34318
    16
    val REMOVED = Value("REMOVED")
wenzelm@34318
    17
    val FAILED = Value("FAILED")
wenzelm@34318
    18
  }
wenzelm@34318
    19
wenzelm@34318
    20
  private var nextId : Long = 0
wenzelm@34318
    21
  def generateId : Long = {
wenzelm@34318
    22
    nextId = nextId + 1
wenzelm@34318
    23
    return nextId
wenzelm@34318
    24
  }
wenzelm@34318
    25
  
wenzelm@34318
    26
  def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
wenzelm@34318
    27
}
wenzelm@34318
    28
wenzelm@34318
    29
class Command(val first : Token[Command], val last : Token[Command]) {
wenzelm@34318
    30
  import Command._
wenzelm@34318
    31
  
wenzelm@34318
    32
  {
wenzelm@34318
    33
    var t = first
wenzelm@34318
    34
    while(t != null) {
wenzelm@34318
    35
      t.command = this
wenzelm@34318
    36
      t = if (t == last) null else t.next
wenzelm@34318
    37
    }
wenzelm@34318
    38
  }
wenzelm@34318
    39
  
wenzelm@34318
    40
  val id : Long = generateId
wenzelm@34318
    41
  var phase = Phase.UNPROCESSED
wenzelm@34318
    42
	
wenzelm@34318
    43
  var results = Nil : List[XML.Tree]
immler@34391
    44
immler@34391
    45
  //offsets relative to first.start!
immler@34391
    46
  class Status(val kind : String,val start : Int, val stop : Int ) { }
immler@34391
    47
  var statuses = Nil : List[Status]
immler@34391
    48
  def statusesxml = XML.Elem("statuses", List(), statuses.map (s => XML.Text(s.kind + ": " + s.start + "-" + s.stop + "\n")))
immler@34391
    49
wenzelm@34318
    50
  def idString = java.lang.Long.toString(id, 36)
wenzelm@34318
    51
  def document = XML.document(results match {
wenzelm@34318
    52
                                case Nil => XML.Elem("message", List(), List())
wenzelm@34318
    53
                                case List(elem) => elem
immler@34391
    54
                                case _ =>
wenzelm@34318
    55
                                  XML.Elem("messages", List(), List(results.first,
wenzelm@34318
    56
                                                                    results.last))
wenzelm@34318
    57
                              }, "style")
wenzelm@34318
    58
  def addResult(tree : XML.Tree) {
wenzelm@34318
    59
    results = results ::: List(tree)
wenzelm@34318
    60
  }
immler@34393
    61
  
immler@34393
    62
  val root_node = {
immler@34393
    63
    val content = Plugin.plugin.prover.document.getContent(this)
immler@34393
    64
    val ra = new RelativeAsset(this, 0, stop - start, "command", content)
immler@34393
    65
    new DefaultMutableTreeNode(ra)
immler@34393
    66
  }
wenzelm@34318
    67
immler@34393
    68
  // does cand fit into node?
immler@34393
    69
  private def fitting(cand : DefaultMutableTreeNode, node : DefaultMutableTreeNode) : boolean = {
immler@34393
    70
    val node_asset = node.getUserObject.asInstanceOf[RelativeAsset]
immler@34393
    71
    val n_start = node_asset.rel_start
immler@34393
    72
    val n_end = node_asset.rel_end
immler@34393
    73
    val cand_asset = cand.getUserObject.asInstanceOf[RelativeAsset]
immler@34393
    74
    val c_start = cand_asset.rel_start
immler@34393
    75
    val c_end = cand_asset.rel_end
immler@34396
    76
    System.err.println(c_start - n_start + " " + (c_end - n_end))
immler@34393
    77
    return c_start >= n_start && c_end <= n_end
immler@34393
    78
  }
immler@34393
    79
immler@34393
    80
  def insert_node(new_node : DefaultMutableTreeNode, node : DefaultMutableTreeNode) {
immler@34393
    81
    assert(fitting(new_node, node))
immler@34393
    82
    val children = node.children
immler@34393
    83
    while (children.hasMoreElements){
immler@34393
    84
      val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode]
immler@34393
    85
      if(fitting(new_node, child)) {
immler@34393
    86
        insert_node(new_node, child)
immler@34393
    87
      }
immler@34393
    88
    }
immler@34393
    89
    if(new_node.getParent == null){
immler@34393
    90
      while(children.hasMoreElements){
immler@34393
    91
        val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode]
immler@34393
    92
        if(fitting(child, new_node)) {
immler@34393
    93
          node.remove(child.asInstanceOf[DefaultMutableTreeNode])
immler@34393
    94
          new_node.add(child)
immler@34393
    95
        }
immler@34393
    96
      }
immler@34393
    97
      node.add(new_node)
immler@34393
    98
    }
immler@34393
    99
  }
immler@34393
   100
immler@34393
   101
 def addStatus(tree : XML.Tree) {
immler@34391
   102
    val (markup_info, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
immler@34391
   103
                                   case _ => null}
immler@34391
   104
immler@34391
   105
    //process attributes:
immler@34391
   106
    var markup_begin = -1
immler@34391
   107
    var markup_end = -1
immler@34391
   108
    for((n, a) <- attr) {
immler@34396
   109
      if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - 1
immler@34396
   110
      if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - 1
immler@34391
   111
    }
immler@34391
   112
    if(markup_begin > -1 && markup_end > -1){
immler@34393
   113
      statuses = new Status(markup_info, markup_begin, markup_end) :: statuses
immler@34396
   114
      val markup_content = content.substring(markup_begin, markup_end)
immler@34396
   115
      val asset = new RelativeAsset(this, markup_begin, markup_end, markup_info, markup_content)
immler@34393
   116
      val new_node = new DefaultMutableTreeNode(asset)
immler@34393
   117
      insert_node(new_node, root_node)
immler@34391
   118
    }
immler@34391
   119
  }
immler@34391
   120
immler@34396
   121
  def content = Plugin.plugin.prover.document.getContent(this)
immler@34396
   122
wenzelm@34318
   123
  def next = if (last.next != null) last.next.command else null
wenzelm@34318
   124
  def previous = if (first.previous != null) first.previous.command else null
wenzelm@34318
   125
wenzelm@34318
   126
  def start = first start
wenzelm@34318
   127
  def stop = last stop
wenzelm@34318
   128
  
wenzelm@34318
   129
  def properStart = start
wenzelm@34318
   130
  def properStop = {
wenzelm@34318
   131
    var i = last
immler@34388
   132
    while (i != first && i.kind.equals(Token.Kind.COMMENT))
wenzelm@34318
   133
      i = i.previous
wenzelm@34318
   134
    i.stop
wenzelm@34318
   135
  }  	
wenzelm@34318
   136
}