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