src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Sat Jul 04 14:14:37 2009 +0200 (2009-07-04)
changeset 34637 f3b5d6e248be
parent 34603 83a37e3b8c9c
child 34653 2e033aaf128e
permissions -rw-r--r--
added symbol_index (presently unused);
misc tuning;
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@34637
    23
object Command
wenzelm@34637
    24
{
wenzelm@34637
    25
  object Status extends Enumeration
wenzelm@34637
    26
  {
wenzelm@34318
    27
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    28
    val FINISHED = Value("FINISHED")
wenzelm@34318
    29
    val FAILED = Value("FAILED")
wenzelm@34318
    30
  }
wenzelm@34318
    31
}
wenzelm@34318
    32
wenzelm@34451
    33
immler@34554
    34
class Command(val tokens: List[Token], val starts: Map[Token, Int])
wenzelm@34451
    35
{
wenzelm@34637
    36
  require(!tokens.isEmpty)
wenzelm@34637
    37
wenzelm@34603
    38
  val id = Isabelle.system.id()
wenzelm@34500
    39
wenzelm@34637
    40
wenzelm@34500
    41
  /* content */
wenzelm@34500
    42
wenzelm@34495
    43
  override def toString = name
wenzelm@34495
    44
immler@34526
    45
  val name = tokens.head.content
wenzelm@34582
    46
  val content: String = Token.string_from_tokens(tokens, starts)
wenzelm@34637
    47
  val symbol_index = new Symbol.Index(content)
wenzelm@34451
    48
immler@34554
    49
  def start(doc: ProofDocument) = doc.token_start(tokens.first)
immler@34554
    50
  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
wenzelm@34451
    51
immler@34593
    52
  def contains(p: Token) = tokens.contains(p)
immler@34593
    53
wenzelm@34637
    54
wenzelm@34637
    55
  /* command status */   // FIXME class Command_State, multiple states per command
wenzelm@34500
    56
wenzelm@34508
    57
  var state_id: IsarDocument.State_ID = null
wenzelm@34508
    58
wenzelm@34500
    59
  private var _status = Command.Status.UNPROCESSED
wenzelm@34500
    60
  def status = _status
wenzelm@34500
    61
  def status_=(st: Command.Status.Value) {
wenzelm@34500
    62
    if (st == Command.Status.UNPROCESSED) {
wenzelm@34533
    63
      state_results.clear
wenzelm@34500
    64
      // delete markup
immler@34577
    65
      markup_root = markup_root.filter(_.info match {
immler@34564
    66
          case RootInfo() | OuterInfo(_) => true
immler@34560
    67
          case _ => false
immler@34577
    68
        }).head
wenzelm@34500
    69
    }
wenzelm@34500
    70
    _status = st
wenzelm@34500
    71
  }
wenzelm@34500
    72
wenzelm@34500
    73
wenzelm@34500
    74
  /* results */
wenzelm@34500
    75
wenzelm@34500
    76
  private val results = new mutable.ListBuffer[XML.Tree]
wenzelm@34500
    77
  private val state_results = new mutable.ListBuffer[XML.Tree]
wenzelm@34533
    78
  def add_result(running: Boolean, tree: XML.Tree) = synchronized {
wenzelm@34508
    79
    (if (running) state_results else results) += tree
wenzelm@34508
    80
  }
wenzelm@34500
    81
wenzelm@34500
    82
  def result_document = XML.document(
wenzelm@34500
    83
    results.toList ::: state_results.toList match {
wenzelm@34500
    84
      case Nil => XML.Elem("message", Nil, Nil)
wenzelm@34500
    85
      case List(elem) => elem
wenzelm@34500
    86
      case elems => XML.Elem("messages", Nil, elems)
wenzelm@34500
    87
    }, "style")
wenzelm@34500
    88
wenzelm@34500
    89
wenzelm@34500
    90
  /* markup */
wenzelm@34451
    91
immler@34557
    92
  val empty_root_node =
wenzelm@34582
    93
    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
wenzelm@34582
    94
      Nil, id, content, RootInfo())
immler@34557
    95
immler@34560
    96
  var markup_root = empty_root_node
wenzelm@34451
    97
wenzelm@34637
    98
  def highlight_node: MarkupNode =
wenzelm@34637
    99
  {
immler@34560
   100
    import MarkupNode._
immler@34564
   101
    markup_root.filter(_.info match {
immler@34564
   102
      case RootInfo() | OuterInfo(_) | HighlightInfo(_) => true
immler@34560
   103
      case _ => false
immler@34560
   104
    }).head
immler@34560
   105
  }
immler@34556
   106
immler@34564
   107
  def markup_node(begin: Int, end: Int, info: MarkupInfo) =
immler@34557
   108
    new MarkupNode(this, begin, end, Nil, id,
wenzelm@34582
   109
      if (end <= content.length && begin >= 0) content.substring(begin, end)
wenzelm@34582
   110
      else "wrong indices??",
wenzelm@34582
   111
      info)
immler@34556
   112
wenzelm@34637
   113
  def type_at(pos: Int): String =
wenzelm@34637
   114
  {
wenzelm@34582
   115
    val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })
immler@34562
   116
    types.flatten(_.flatten).
immler@34562
   117
      find(t => t.start <= pos && t.stop > pos).
wenzelm@34586
   118
      map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })).
immler@34562
   119
      getOrElse(null)
immler@34562
   120
  }
immler@34568
   121
immler@34568
   122
  def ref_at(pos: Int): Option[MarkupNode] =
wenzelm@34582
   123
    markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
immler@34568
   124
      flatten(_.flatten).
immler@34568
   125
      find(t => t.start <= pos && t.stop > pos)
wenzelm@34451
   126
}