src/Tools/jEdit/src/prover/Command.scala
author immler@in.tum.de
Wed Dec 10 14:45:04 2008 +0100 (2008-12-10 ago)
changeset 34401 44241a37b74a
parent 34400 1b61a92f8675
child 34407 aad6834ba380
permissions -rw-r--r--
structure of markup-tree in scala, keep track of swing-nodes in background
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@34400
     6
import sidekick.{SideKickParsedData, IAsset}
immler@34393
     7
import javax.swing.text.Position
immler@34393
     8
import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34318
     9
wenzelm@34318
    10
object Command {
wenzelm@34318
    11
  object Phase extends Enumeration {
wenzelm@34318
    12
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    13
    val FINISHED = Value("FINISHED")
wenzelm@34318
    14
    val REMOVE = Value("REMOVE")
wenzelm@34318
    15
    val REMOVED = Value("REMOVED")
wenzelm@34318
    16
    val FAILED = Value("FAILED")
wenzelm@34318
    17
  }
wenzelm@34318
    18
wenzelm@34318
    19
  private var nextId : Long = 0
wenzelm@34318
    20
  def generateId : Long = {
wenzelm@34318
    21
    nextId = nextId + 1
wenzelm@34318
    22
    return nextId
wenzelm@34318
    23
  }
wenzelm@34318
    24
  
wenzelm@34318
    25
  def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
wenzelm@34318
    26
}
wenzelm@34318
    27
immler@34397
    28
class Command(val document : Document, val first : Token[Command], val last : Token[Command]) {
wenzelm@34318
    29
  import Command._
wenzelm@34318
    30
  
wenzelm@34318
    31
  {
wenzelm@34318
    32
    var t = first
wenzelm@34318
    33
    while(t != null) {
wenzelm@34318
    34
      t.command = this
wenzelm@34318
    35
      t = if (t == last) null else t.next
wenzelm@34318
    36
    }
wenzelm@34318
    37
  }
wenzelm@34318
    38
  
wenzelm@34318
    39
  val id : Long = generateId
immler@34399
    40
immler@34399
    41
  private var p = Phase.UNPROCESSED
immler@34399
    42
  def phase = p
immler@34399
    43
  def phase_=(p_new : Phase.Value) = {
immler@34399
    44
    if(p_new == Phase.UNPROCESSED){
immler@34399
    45
      //delete inner syntax
immler@34401
    46
      for(child <- root_node.children){
immler@34401
    47
        child.children = Nil
immler@34399
    48
      }
immler@34399
    49
    }
immler@34399
    50
    p = p_new
immler@34399
    51
  }
wenzelm@34318
    52
	
wenzelm@34318
    53
  var results = Nil : List[XML.Tree]
immler@34391
    54
wenzelm@34318
    55
  def idString = java.lang.Long.toString(id, 36)
immler@34397
    56
  def results_xml = XML.document(results match {
wenzelm@34318
    57
                                case Nil => XML.Elem("message", List(), List())
wenzelm@34318
    58
                                case List(elem) => elem
immler@34391
    59
                                case _ =>
wenzelm@34318
    60
                                  XML.Elem("messages", List(), List(results.first,
wenzelm@34318
    61
                                                                    results.last))
wenzelm@34318
    62
                              }, "style")
wenzelm@34318
    63
  def addResult(tree : XML.Tree) {
wenzelm@34318
    64
    results = results ::: List(tree)
wenzelm@34318
    65
  }
immler@34393
    66
  
immler@34400
    67
  val root_node = 
immler@34400
    68
    new MarkupNode(this, 0, stop - start, idString, "Command", document.getContent(this))
immler@34393
    69
immler@34400
    70
  def node_from(kind : String, begin : Int, end : Int) : MarkupNode = {
immler@34400
    71
    val markup_content = /*content.substring(begin, end)*/ ""
immler@34400
    72
    new MarkupNode(this, begin, end, idString, kind, markup_content)
immler@34391
    73
  }
immler@34391
    74
immler@34397
    75
  def content = document.getContent(this)
immler@34396
    76
wenzelm@34318
    77
  def next = if (last.next != null) last.next.command else null
wenzelm@34318
    78
  def previous = if (first.previous != null) first.previous.command else null
wenzelm@34318
    79
wenzelm@34318
    80
  def start = first start
wenzelm@34318
    81
  def stop = last stop
wenzelm@34318
    82
  
wenzelm@34318
    83
  def properStart = start
wenzelm@34318
    84
  def properStop = {
wenzelm@34318
    85
    var i = last
immler@34388
    86
    while (i != first && i.kind.equals(Token.Kind.COMMENT))
wenzelm@34318
    87
      i = i.previous
wenzelm@34318
    88
    i.stop
wenzelm@34318
    89
  }  	
wenzelm@34318
    90
}