src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Sat Sep 05 00:35:37 2009 +0200 (2009-09-05)
changeset 34707 cc5d388fcbf2
parent 34705 cd2cdf3b33b9
child 34708 611864f2729d
permissions -rw-r--r--
eliminated MarkupInfo, moved particular variants into object Command;
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@34707
    46
wenzelm@34707
    47
  case object RootInfo
wenzelm@34707
    48
  case class HighlightInfo(highlight: String) { override def toString = highlight }
wenzelm@34707
    49
  case class TypeInfo(type_kind: String) { override def toString = type_kind }
wenzelm@34707
    50
  case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@34707
    51
    command_id: Option[String], offset: Option[Int]) {
wenzelm@34707
    52
      override def toString = (file, line, command_id, offset).toString
wenzelm@34707
    53
    }
wenzelm@34318
    54
}
wenzelm@34318
    55
wenzelm@34451
    56
wenzelm@34697
    57
class Command(
wenzelm@34697
    58
  val tokens: List[Token],
wenzelm@34697
    59
  val starts: Map[Token, Int],
wenzelm@34697
    60
  change_receiver: Actor) extends Accumulator
wenzelm@34451
    61
{
wenzelm@34637
    62
  require(!tokens.isEmpty)
wenzelm@34637
    63
wenzelm@34603
    64
  val id = Isabelle.system.id()
immler@34653
    65
  override def hashCode = id.hashCode
wenzelm@34637
    66
wenzelm@34697
    67
  def changed() = change_receiver ! this
immler@34674
    68
immler@34674
    69
wenzelm@34500
    70
  /* content */
wenzelm@34500
    71
wenzelm@34495
    72
  override def toString = name
wenzelm@34495
    73
immler@34526
    74
  val name = tokens.head.content
wenzelm@34582
    75
  val content: String = Token.string_from_tokens(tokens, starts)
wenzelm@34637
    76
  val symbol_index = new Symbol.Index(content)
wenzelm@34451
    77
immler@34554
    78
  def start(doc: ProofDocument) = doc.token_start(tokens.first)
immler@34554
    79
  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
wenzelm@34451
    80
immler@34593
    81
  def contains(p: Token) = tokens.contains(p)
immler@34593
    82
wenzelm@34697
    83
  protected override var _state = new State(this)
immler@34676
    84
immler@34676
    85
immler@34676
    86
  /* markup */
wenzelm@34508
    87
immler@34676
    88
  lazy val empty_root_node =
wenzelm@34704
    89
    new MarkupNode(0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
wenzelm@34707
    90
      Nil, content, Command.RootInfo)
immler@34676
    91
wenzelm@34707
    92
  def markup_node(begin: Int, end: Int, info: Any): MarkupNode =
wenzelm@34699
    93
  {
wenzelm@34703
    94
    val start = symbol_index.decode(begin)
wenzelm@34703
    95
    val stop = symbol_index.decode(end)
wenzelm@34705
    96
    new MarkupNode(start, stop, Nil, content.substring(start, stop), info)
wenzelm@34500
    97
  }
wenzelm@34500
    98
immler@34676
    99
immler@34676
   100
  /* results, markup, ... */
wenzelm@34500
   101
immler@34676
   102
  private val empty_cmd_state = new Command_State(this)
immler@34676
   103
  private def cmd_state(doc: ProofDocument) =
immler@34676
   104
    doc.states.getOrElse(this, empty_cmd_state)
wenzelm@34500
   105
immler@34676
   106
  def status(doc: ProofDocument) = cmd_state(doc).state.status
immler@34676
   107
  def result_document(doc: ProofDocument) = cmd_state(doc).result_document
immler@34676
   108
  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
immler@34676
   109
  def highlight_node(doc: ProofDocument) = cmd_state(doc).highlight_node
immler@34676
   110
  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
immler@34676
   111
  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
immler@34676
   112
}
immler@34676
   113
wenzelm@34500
   114
wenzelm@34698
   115
class Command_State(val command: Command) extends Accumulator
immler@34676
   116
{
wenzelm@34698
   117
  protected override var _state = new State(command)
immler@34676
   118
wenzelm@34698
   119
  def result_document: org.w3c.dom.Document =
immler@34653
   120
    XML.document(
wenzelm@34698
   121
      command.state.results ::: state.results match {
immler@34653
   122
        case Nil => XML.Elem("message", Nil, Nil)
immler@34653
   123
        case List(elem) => elem
immler@34653
   124
        case elems => XML.Elem("messages", Nil, elems)
immler@34653
   125
      }, "style")
wenzelm@34500
   126
immler@34688
   127
  def markup_root: MarkupNode =
wenzelm@34699
   128
    (command.state.markup_root /: state.markup_root.children)(_ + _)
immler@34557
   129
immler@34688
   130
  def type_at(pos: Int): String = state.type_at(pos)
immler@34556
   131
immler@34688
   132
  def ref_at(pos: Int): Option[MarkupNode] = state.ref_at(pos)
immler@34568
   133
wenzelm@34698
   134
  def highlight_node: MarkupNode =
wenzelm@34699
   135
    (command.state.highlight_node /: state.highlight_node.children)(_ + _)
immler@34688
   136
}