src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Tue Jan 20 22:55:45 2009 +0100 (2009-01-20 ago)
changeset 34495 722533c532da
parent 34491 20e9d420dbbb
child 34497 184fda8cce04
child 34510 6106e71c6ee5
permissions -rw-r--r--
Command: added name field and toString;
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@34486
    14
import scala.collection.mutable.ListBuffer
wenzelm@34486
    15
wenzelm@34491
    16
import isabelle.proofdocument.{Text, Token, ProofDocument}
wenzelm@34451
    17
import isabelle.jedit.{Isabelle, Plugin}
wenzelm@34476
    18
import isabelle.XML
wenzelm@34451
    19
wenzelm@34451
    20
import sidekick.{SideKickParsedData, IAsset}
wenzelm@34451
    21
wenzelm@34451
    22
wenzelm@34318
    23
object Command {
wenzelm@34458
    24
  object Status extends Enumeration {
wenzelm@34318
    25
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    26
    val FINISHED = Value("FINISHED")
wenzelm@34318
    27
    val REMOVE = Value("REMOVE")
wenzelm@34318
    28
    val REMOVED = Value("REMOVED")
wenzelm@34318
    29
    val FAILED = Value("FAILED")
wenzelm@34318
    30
  }
wenzelm@34318
    31
}
wenzelm@34318
    32
wenzelm@34451
    33
wenzelm@34491
    34
class Command(text: Text, val first: Token, val last: Token)
wenzelm@34451
    35
{
wenzelm@34451
    36
  val id = Isabelle.plugin.id()
wenzelm@34318
    37
  
wenzelm@34318
    38
  {
wenzelm@34318
    39
    var t = first
wenzelm@34451
    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@34451
    45
immler@34399
    46
wenzelm@34458
    47
  /* command status */
wenzelm@34451
    48
wenzelm@34458
    49
  private var _status = Command.Status.UNPROCESSED
wenzelm@34458
    50
  def status = _status
wenzelm@34458
    51
  def status_=(st: Command.Status.Value) = {
wenzelm@34458
    52
    if (st == Command.Status.UNPROCESSED) {
wenzelm@34451
    53
      // delete markup
wenzelm@34451
    54
      for (child <- root_node.children) {
immler@34401
    55
        child.children = Nil
immler@34399
    56
      }
immler@34399
    57
    }
wenzelm@34458
    58
    _status = st
immler@34399
    59
  }
wenzelm@34451
    60
immler@34391
    61
wenzelm@34451
    62
  /* accumulated results */
wenzelm@34451
    63
wenzelm@34486
    64
  private val results = new ListBuffer[XML.Tree]
wenzelm@34486
    65
  def add_result(tree: XML.Tree) { results += tree }
wenzelm@34451
    66
wenzelm@34486
    67
  def result_document = XML.document(
wenzelm@34486
    68
    results.toList match {
wenzelm@34410
    69
      case Nil => XML.Elem("message", Nil, Nil)
wenzelm@34410
    70
      case List(elem) => elem
wenzelm@34486
    71
      case elems => XML.Elem("messages", Nil, List(elems.first, elems.last))  // FIXME all elems!?
wenzelm@34410
    72
    }, "style")
wenzelm@34451
    73
immler@34393
    74
wenzelm@34451
    75
  /* content */
immler@34391
    76
wenzelm@34495
    77
  override def toString = name
wenzelm@34495
    78
wenzelm@34495
    79
  val name = text.content(first.start, first.stop)
wenzelm@34491
    80
  val content = text.content(proper_start, proper_stop)
immler@34396
    81
wenzelm@34318
    82
  def next = if (last.next != null) last.next.command else null
wenzelm@34483
    83
  def prev = if (first.prev != null) first.prev.command else null
wenzelm@34318
    84
wenzelm@34451
    85
  def start = first.start
wenzelm@34451
    86
  def stop = last.stop
wenzelm@34451
    87
wenzelm@34451
    88
  def proper_start = start
wenzelm@34451
    89
  def proper_stop = {
wenzelm@34318
    90
    var i = last
wenzelm@34484
    91
    while (i != first && i.kind == Token.Kind.COMMENT)
wenzelm@34483
    92
      i = i.prev
wenzelm@34318
    93
    i.stop
wenzelm@34451
    94
  }
wenzelm@34451
    95
wenzelm@34451
    96
wenzelm@34451
    97
  /* markup tree */
wenzelm@34451
    98
wenzelm@34451
    99
  val root_node =
wenzelm@34491
   100
    new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
wenzelm@34451
   101
wenzelm@34451
   102
  def node_from(kind: String, begin: Int, end: Int) = {
wenzelm@34451
   103
    val markup_content = /*content.substring(begin, end)*/ ""
wenzelm@34451
   104
    new MarkupNode(this, begin, end, id, kind, markup_content)
wenzelm@34451
   105
  }
wenzelm@34451
   106
}