src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Mon Jan 19 21:58:38 2009 +0100 (2009-01-19 ago)
changeset 34484 920ff05ca3f3
parent 34483 0923926022d7
child 34485 6475bfb4ff99
permissions -rw-r--r--
eliminated explicit method equals, which is always behind == / != anyway in Scala;
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@34451
    10
immler@34393
    11
import javax.swing.text.Position
immler@34393
    12
import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34318
    13
wenzelm@34451
    14
import isabelle.proofdocument.Token
wenzelm@34451
    15
import isabelle.jedit.{Isabelle, Plugin}
wenzelm@34476
    16
import isabelle.XML
wenzelm@34451
    17
wenzelm@34451
    18
import sidekick.{SideKickParsedData, IAsset}
wenzelm@34451
    19
wenzelm@34451
    20
wenzelm@34318
    21
object Command {
wenzelm@34458
    22
  object Status extends Enumeration {
wenzelm@34318
    23
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    24
    val FINISHED = Value("FINISHED")
wenzelm@34318
    25
    val REMOVE = Value("REMOVE")
wenzelm@34318
    26
    val REMOVED = Value("REMOVED")
wenzelm@34318
    27
    val FAILED = Value("FAILED")
wenzelm@34318
    28
  }
wenzelm@34318
    29
}
wenzelm@34318
    30
wenzelm@34451
    31
wenzelm@34481
    32
class Command(val document: Document, val first: Token, val last: Token)
wenzelm@34451
    33
{
wenzelm@34451
    34
  val id = Isabelle.plugin.id()
wenzelm@34318
    35
  
wenzelm@34318
    36
  {
wenzelm@34318
    37
    var t = first
wenzelm@34451
    38
    while (t != null) {
wenzelm@34318
    39
      t.command = this
wenzelm@34318
    40
      t = if (t == last) null else t.next
wenzelm@34318
    41
    }
wenzelm@34318
    42
  }
wenzelm@34451
    43
immler@34399
    44
wenzelm@34458
    45
  /* command status */
wenzelm@34451
    46
wenzelm@34458
    47
  private var _status = Command.Status.UNPROCESSED
wenzelm@34458
    48
  def status = _status
wenzelm@34458
    49
  def status_=(st: Command.Status.Value) = {
wenzelm@34458
    50
    if (st == Command.Status.UNPROCESSED) {
wenzelm@34451
    51
      // delete markup
wenzelm@34451
    52
      for (child <- root_node.children) {
immler@34401
    53
        child.children = Nil
immler@34399
    54
      }
immler@34399
    55
    }
wenzelm@34458
    56
    _status = st
immler@34399
    57
  }
wenzelm@34451
    58
immler@34391
    59
wenzelm@34451
    60
  /* accumulated results */
wenzelm@34451
    61
wenzelm@34451
    62
  var results: List[XML.Tree] = Nil
wenzelm@34451
    63
wenzelm@34410
    64
  def results_xml = XML.document(
wenzelm@34410
    65
    results match {
wenzelm@34410
    66
      case Nil => XML.Elem("message", Nil, Nil)
wenzelm@34410
    67
      case List(elem) => elem
wenzelm@34451
    68
      case _ => XML.Elem("messages", Nil, List(results.first, results.last))
wenzelm@34410
    69
    }, "style")
wenzelm@34451
    70
  def add_result(tree: XML.Tree) {
wenzelm@34410
    71
    results = results ::: List(tree)    // FIXME canonical reverse order
wenzelm@34318
    72
  }
wenzelm@34451
    73
immler@34393
    74
wenzelm@34451
    75
  /* content */
immler@34391
    76
wenzelm@34451
    77
  def content(): String = document.getContent(this)
immler@34396
    78
wenzelm@34318
    79
  def next = if (last.next != null) last.next.command else null
wenzelm@34483
    80
  def prev = if (first.prev != null) first.prev.command else null
wenzelm@34318
    81
wenzelm@34451
    82
  def start = first.start
wenzelm@34451
    83
  def stop = last.stop
wenzelm@34451
    84
wenzelm@34451
    85
  def proper_start = start
wenzelm@34451
    86
  def proper_stop = {
wenzelm@34318
    87
    var i = last
wenzelm@34484
    88
    while (i != first && i.kind == Token.Kind.COMMENT)
wenzelm@34483
    89
      i = i.prev
wenzelm@34318
    90
    i.stop
wenzelm@34451
    91
  }
wenzelm@34451
    92
wenzelm@34451
    93
wenzelm@34451
    94
  /* markup tree */
wenzelm@34451
    95
wenzelm@34451
    96
  val root_node =
wenzelm@34451
    97
    new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content())
wenzelm@34451
    98
wenzelm@34451
    99
  def node_from(kind: String, begin: Int, end: Int) = {
wenzelm@34451
   100
    val markup_content = /*content.substring(begin, end)*/ ""
wenzelm@34451
   101
    new MarkupNode(this, begin, end, id, kind, markup_content)
wenzelm@34451
   102
  }
wenzelm@34451
   103
}