src/Tools/jEdit/src/prover/Command.scala
author immler@in.tum.de
Fri Nov 28 17:49:39 2008 +0100 (2008-11-28 ago)
changeset 34391 7b5f44553aaf
parent 34388 23b8351ecbbe
child 34393 f0e1608a774f
permissions -rw-r--r--
ugly fine-grained buffer markup
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]
immler@34391
    39
immler@34391
    40
  //offsets relative to first.start!
immler@34391
    41
  class Status(val kind : String,val start : Int, val stop : Int ) { }
immler@34391
    42
  var statuses = Nil : List[Status]
immler@34391
    43
  def statusesxml = XML.Elem("statuses", List(), statuses.map (s => XML.Text(s.kind + ": " + s.start + "-" + s.stop + "\n")))
immler@34391
    44
wenzelm@34318
    45
  def idString = java.lang.Long.toString(id, 36)
wenzelm@34318
    46
  def document = XML.document(results match {
wenzelm@34318
    47
                                case Nil => XML.Elem("message", List(), List())
wenzelm@34318
    48
                                case List(elem) => elem
immler@34391
    49
                                case _ =>
wenzelm@34318
    50
                                  XML.Elem("messages", List(), List(results.first,
wenzelm@34318
    51
                                                                    results.last))
wenzelm@34318
    52
                              }, "style")
wenzelm@34318
    53
  def addResult(tree : XML.Tree) {
wenzelm@34318
    54
    results = results ::: List(tree)
wenzelm@34318
    55
  }
wenzelm@34318
    56
immler@34391
    57
  def addStatus(tree : XML.Tree) {
immler@34391
    58
    val (markup_info, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
immler@34391
    59
                                   case _ => null}
immler@34391
    60
immler@34391
    61
    //process attributes:
immler@34391
    62
    var markup_begin = -1
immler@34391
    63
    var markup_end = -1
immler@34391
    64
    for((n, a) <- attr) {
immler@34391
    65
      if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - first.start
immler@34391
    66
      if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - first.start
immler@34391
    67
    }
immler@34391
    68
    if(markup_begin > -1 && markup_end > -1){
immler@34391
    69
          statuses = new Status(markup_info, markup_begin, markup_end) :: statuses
immler@34391
    70
    }
immler@34391
    71
  }
immler@34391
    72
wenzelm@34318
    73
  def next = if (last.next != null) last.next.command else null
wenzelm@34318
    74
  def previous = if (first.previous != null) first.previous.command else null
wenzelm@34318
    75
wenzelm@34318
    76
  def start = first start
wenzelm@34318
    77
  def stop = last stop
wenzelm@34318
    78
  
wenzelm@34318
    79
  def properStart = start
wenzelm@34318
    80
  def properStop = {
wenzelm@34318
    81
    var i = last
immler@34388
    82
    while (i != first && i.kind.equals(Token.Kind.COMMENT))
wenzelm@34318
    83
      i = i.previous
wenzelm@34318
    84
    i.stop
wenzelm@34318
    85
  }  	
wenzelm@34318
    86
}