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