src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Thu Sep 03 16:47:42 2009 +0200 (2009-09-03 ago)
changeset 34699 9a4e5f93ccb6
parent 34698 33286290e3b0
child 34703 ff037c17332a
permissions -rw-r--r--
tuned;
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
wenzelm@34699
    11
import scala.actors.Actor, Actor._
wenzelm@34318
    12
wenzelm@34497
    13
import scala.collection.mutable
wenzelm@34486
    14
immler@34662
    15
import isabelle.proofdocument.{Token, ProofDocument}
wenzelm@34451
    16
import isabelle.jedit.{Isabelle, Plugin}
wenzelm@34476
    17
import isabelle.XML
wenzelm@34451
    18
wenzelm@34451
    19
immler@34675
    20
trait Accumulator extends Actor
immler@34675
    21
{
immler@34675
    22
immler@34675
    23
  start() // start actor
immler@34675
    24
immler@34675
    25
  protected var _state: State
immler@34675
    26
  def state = _state
immler@34675
    27
immler@34675
    28
  override def act() {
immler@34675
    29
    loop {
immler@34675
    30
      react {
wenzelm@34697
    31
        case message: XML.Tree => _state += message
immler@34675
    32
      }
immler@34675
    33
    }
immler@34675
    34
  }
immler@34675
    35
}
immler@34675
    36
wenzelm@34451
    37
wenzelm@34637
    38
object Command
wenzelm@34637
    39
{
wenzelm@34637
    40
  object Status extends Enumeration
wenzelm@34637
    41
  {
wenzelm@34318
    42
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    43
    val FINISHED = Value("FINISHED")
wenzelm@34318
    44
    val FAILED = Value("FAILED")
wenzelm@34318
    45
  }
wenzelm@34318
    46
}
wenzelm@34318
    47
wenzelm@34451
    48
wenzelm@34697
    49
class Command(
wenzelm@34697
    50
  val tokens: List[Token],
wenzelm@34697
    51
  val starts: Map[Token, Int],
wenzelm@34697
    52
  change_receiver: Actor) extends Accumulator
wenzelm@34451
    53
{
wenzelm@34637
    54
  require(!tokens.isEmpty)
wenzelm@34637
    55
wenzelm@34603
    56
  val id = Isabelle.system.id()
immler@34653
    57
  override def hashCode = id.hashCode
wenzelm@34637
    58
wenzelm@34697
    59
  def changed() = change_receiver ! this
immler@34674
    60
immler@34674
    61
wenzelm@34500
    62
  /* content */
wenzelm@34500
    63
wenzelm@34495
    64
  override def toString = name
wenzelm@34495
    65
immler@34526
    66
  val name = tokens.head.content
wenzelm@34582
    67
  val content: String = Token.string_from_tokens(tokens, starts)
wenzelm@34637
    68
  val symbol_index = new Symbol.Index(content)
wenzelm@34451
    69
immler@34554
    70
  def start(doc: ProofDocument) = doc.token_start(tokens.first)
immler@34554
    71
  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
wenzelm@34451
    72
immler@34593
    73
  def contains(p: Token) = tokens.contains(p)
immler@34593
    74
wenzelm@34697
    75
  protected override var _state = new State(this)
immler@34676
    76
immler@34676
    77
immler@34676
    78
  /* markup */
wenzelm@34508
    79
immler@34676
    80
  lazy val empty_root_node =
immler@34676
    81
    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
immler@34676
    82
      Nil, id, content, RootInfo())
immler@34676
    83
wenzelm@34699
    84
  def markup_node(begin: Int, end: Int, info: MarkupInfo): MarkupNode =
wenzelm@34699
    85
  {
immler@34676
    86
    new MarkupNode(this, symbol_index.decode(begin), symbol_index.decode(end), Nil, id,
immler@34676
    87
      content.substring(symbol_index.decode(begin), symbol_index.decode(end)),
immler@34676
    88
      info)
wenzelm@34500
    89
  }
wenzelm@34500
    90
immler@34676
    91
immler@34676
    92
  /* results, markup, ... */
wenzelm@34500
    93
immler@34676
    94
  private val empty_cmd_state = new Command_State(this)
immler@34676
    95
  private def cmd_state(doc: ProofDocument) =
immler@34676
    96
    doc.states.getOrElse(this, empty_cmd_state)
wenzelm@34500
    97
immler@34676
    98
  def status(doc: ProofDocument) = cmd_state(doc).state.status
immler@34676
    99
  def result_document(doc: ProofDocument) = cmd_state(doc).result_document
immler@34676
   100
  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
immler@34676
   101
  def highlight_node(doc: ProofDocument) = cmd_state(doc).highlight_node
immler@34676
   102
  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
immler@34676
   103
  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
immler@34676
   104
}
immler@34676
   105
wenzelm@34500
   106
wenzelm@34698
   107
class Command_State(val command: Command) extends Accumulator
immler@34676
   108
{
wenzelm@34698
   109
  protected override var _state = new State(command)
immler@34676
   110
wenzelm@34698
   111
  def result_document: org.w3c.dom.Document =
immler@34653
   112
    XML.document(
wenzelm@34698
   113
      command.state.results ::: state.results match {
immler@34653
   114
        case Nil => XML.Elem("message", Nil, Nil)
immler@34653
   115
        case List(elem) => elem
immler@34653
   116
        case elems => XML.Elem("messages", Nil, elems)
immler@34653
   117
      }, "style")
wenzelm@34500
   118
immler@34688
   119
  def markup_root: MarkupNode =
wenzelm@34699
   120
    (command.state.markup_root /: state.markup_root.children)(_ + _)
immler@34557
   121
immler@34688
   122
  def type_at(pos: Int): String = state.type_at(pos)
immler@34556
   123
immler@34688
   124
  def ref_at(pos: Int): Option[MarkupNode] = state.ref_at(pos)
immler@34568
   125
wenzelm@34698
   126
  def highlight_node: MarkupNode =
wenzelm@34699
   127
    (command.state.highlight_node /: state.highlight_node.children)(_ + _)
immler@34688
   128
}