src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Sun Oct 19 16:51:55 2008 +0200 (2008-10-19 ago)
changeset 34318 c13e168a8ae6
child 34388 23b8351ecbbe
permissions -rw-r--r--
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm@34318
     1
package isabelle.prover
wenzelm@34318
     2
wenzelm@34318
     3
import isabelle.proofdocument.Token
wenzelm@34318
     4
import isabelle.{ YXML, XML }
wenzelm@34318
     5
wenzelm@34318
     6
object Command {
wenzelm@34318
     7
  object Phase extends Enumeration {
wenzelm@34318
     8
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
     9
    val FINISHED = Value("FINISHED")
wenzelm@34318
    10
    val REMOVE = Value("REMOVE")
wenzelm@34318
    11
    val REMOVED = Value("REMOVED")
wenzelm@34318
    12
    val FAILED = Value("FAILED")
wenzelm@34318
    13
  }
wenzelm@34318
    14
wenzelm@34318
    15
  private var nextId : Long = 0
wenzelm@34318
    16
  def generateId : Long = {
wenzelm@34318
    17
    nextId = nextId + 1
wenzelm@34318
    18
    return nextId
wenzelm@34318
    19
  }
wenzelm@34318
    20
  
wenzelm@34318
    21
  def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
wenzelm@34318
    22
}
wenzelm@34318
    23
wenzelm@34318
    24
class Command(val first : Token[Command], val last : Token[Command]) {
wenzelm@34318
    25
  import Command._
wenzelm@34318
    26
  
wenzelm@34318
    27
  {
wenzelm@34318
    28
    var t = first
wenzelm@34318
    29
    while(t != null) {
wenzelm@34318
    30
      t.command = this
wenzelm@34318
    31
      t = if (t == last) null else t.next
wenzelm@34318
    32
    }
wenzelm@34318
    33
  }
wenzelm@34318
    34
  
wenzelm@34318
    35
  val id : Long = generateId
wenzelm@34318
    36
  var phase = Phase.UNPROCESSED
wenzelm@34318
    37
	
wenzelm@34318
    38
  var results = Nil : List[XML.Tree]
wenzelm@34318
    39
  
wenzelm@34318
    40
  def idString = java.lang.Long.toString(id, 36)
wenzelm@34318
    41
  def document = XML.document(results match {
wenzelm@34318
    42
                                case Nil => XML.Elem("message", List(), List())
wenzelm@34318
    43
                                case List(elem) => elem
wenzelm@34318
    44
                                case _ => 
wenzelm@34318
    45
                                  XML.Elem("messages", List(), List(results.first,
wenzelm@34318
    46
                                                                    results.last))
wenzelm@34318
    47
                              }, "style")
wenzelm@34318
    48
  def addResult(tree : XML.Tree) {
wenzelm@34318
    49
    results = results ::: List(tree)
wenzelm@34318
    50
  }
wenzelm@34318
    51
wenzelm@34318
    52
  def next = if (last.next != null) last.next.command else null
wenzelm@34318
    53
  def previous = if (first.previous != null) first.previous.command else null
wenzelm@34318
    54
wenzelm@34318
    55
  def start = first start
wenzelm@34318
    56
  def stop = last stop
wenzelm@34318
    57
  
wenzelm@34318
    58
  def properStart = start
wenzelm@34318
    59
  def properStop = {
wenzelm@34318
    60
    var i = last
wenzelm@34318
    61
    while (i != first && i.isComment)
wenzelm@34318
    62
      i = i.previous
wenzelm@34318
    63
    i.stop
wenzelm@34318
    64
  }  	
wenzelm@34318
    65
}