src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Tue Jan 27 22:16:29 2009 +0100 (2009-01-27 ago)
changeset 34508 422a43b76f77
parent 34500 384427c750c8
child 34511 5839e34ef0bd
child 34533 35308320713a
permissions -rw-r--r--
eliminated Command.Status.REMOVE/REMOVED;
added state_id;
refined add_result: running flag;
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@34497
    14
import scala.collection.mutable
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 FAILED = Value("FAILED")
wenzelm@34318
    28
  }
wenzelm@34318
    29
}
wenzelm@34318
    30
wenzelm@34451
    31
wenzelm@34491
    32
class Command(text: Text, val first: Token, val last: Token)
wenzelm@34451
    33
{
wenzelm@34451
    34
  val id = Isabelle.plugin.id()
wenzelm@34500
    35
wenzelm@34500
    36
wenzelm@34500
    37
  /* content */
wenzelm@34500
    38
wenzelm@34318
    39
  {
wenzelm@34318
    40
    var t = first
wenzelm@34451
    41
    while (t != null) {
wenzelm@34318
    42
      t.command = this
wenzelm@34318
    43
      t = if (t == last) null else t.next
wenzelm@34318
    44
    }
wenzelm@34318
    45
  }
wenzelm@34451
    46
wenzelm@34495
    47
  override def toString = name
wenzelm@34495
    48
wenzelm@34495
    49
  val name = text.content(first.start, first.stop)
wenzelm@34491
    50
  val content = text.content(proper_start, proper_stop)
immler@34396
    51
wenzelm@34318
    52
  def next = if (last.next != null) last.next.command else null
wenzelm@34483
    53
  def prev = if (first.prev != null) first.prev.command else null
wenzelm@34318
    54
wenzelm@34451
    55
  def start = first.start
wenzelm@34451
    56
  def stop = last.stop
wenzelm@34451
    57
wenzelm@34451
    58
  def proper_start = start
wenzelm@34451
    59
  def proper_stop = {
wenzelm@34318
    60
    var i = last
wenzelm@34484
    61
    while (i != first && i.kind == Token.Kind.COMMENT)
wenzelm@34483
    62
      i = i.prev
wenzelm@34318
    63
    i.stop
wenzelm@34451
    64
  }
wenzelm@34451
    65
wenzelm@34451
    66
wenzelm@34500
    67
  /* command status */
wenzelm@34500
    68
wenzelm@34508
    69
  var state_id: IsarDocument.State_ID = null
wenzelm@34508
    70
wenzelm@34500
    71
  private var _status = Command.Status.UNPROCESSED
wenzelm@34500
    72
  def status = _status
wenzelm@34500
    73
  def status_=(st: Command.Status.Value) {
wenzelm@34500
    74
    if (st == Command.Status.UNPROCESSED) {
wenzelm@34500
    75
      // delete markup
wenzelm@34500
    76
      for (child <- root_node.children) {
wenzelm@34500
    77
        child.children = Nil
wenzelm@34500
    78
      }
wenzelm@34500
    79
    }
wenzelm@34500
    80
    _status = st
wenzelm@34500
    81
  }
wenzelm@34500
    82
wenzelm@34500
    83
wenzelm@34500
    84
  /* results */
wenzelm@34500
    85
wenzelm@34500
    86
  private val results = new mutable.ListBuffer[XML.Tree]
wenzelm@34500
    87
  private val state_results = new mutable.ListBuffer[XML.Tree]
wenzelm@34508
    88
  def add_result(running: Boolean, tree: XML.Tree) {
wenzelm@34508
    89
    (if (running) state_results else results) += tree
wenzelm@34508
    90
  }
wenzelm@34500
    91
wenzelm@34500
    92
  def result_document = XML.document(
wenzelm@34500
    93
    results.toList ::: state_results.toList match {
wenzelm@34500
    94
      case Nil => XML.Elem("message", Nil, Nil)
wenzelm@34500
    95
      case List(elem) => elem
wenzelm@34500
    96
      case elems => XML.Elem("messages", Nil, elems)
wenzelm@34500
    97
    }, "style")
wenzelm@34500
    98
wenzelm@34500
    99
wenzelm@34500
   100
  /* markup */
wenzelm@34451
   101
wenzelm@34451
   102
  val root_node =
wenzelm@34491
   103
    new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
wenzelm@34451
   104
wenzelm@34451
   105
  def node_from(kind: String, begin: Int, end: Int) = {
wenzelm@34451
   106
    val markup_content = /*content.substring(begin, end)*/ ""
wenzelm@34451
   107
    new MarkupNode(this, begin, end, id, kind, markup_content)
wenzelm@34451
   108
  }
wenzelm@34451
   109
}