src/Tools/jEdit/src/proofdocument/command.scala
changeset 34759 bfea7839d9e1
parent 34746 94ef0ff39c21
child 34760 dc7f5e0d9d27
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala	Tue Dec 08 14:49:01 2009 +0100
     1.3 @@ -0,0 +1,124 @@
     1.4 +/*
     1.5 + * Prover commands with semantic state
     1.6 + *
     1.7 + * @author Johannes Hölzl, TU Munich
     1.8 + * @author Fabian Immler, TU Munich
     1.9 + */
    1.10 +
    1.11 +package isabelle.prover
    1.12 +
    1.13 +
    1.14 +import scala.actors.Actor, Actor._
    1.15 +
    1.16 +import scala.collection.mutable
    1.17 +
    1.18 +import isabelle.proofdocument.{Token, ProofDocument}
    1.19 +import isabelle.jedit.{Isabelle, Plugin}
    1.20 +import isabelle.XML
    1.21 +
    1.22 +
    1.23 +trait Accumulator extends Actor
    1.24 +{
    1.25 +  start() // start actor
    1.26 +
    1.27 +  protected var _state: State
    1.28 +  def state = _state
    1.29 +
    1.30 +  override def act() {
    1.31 +    loop {
    1.32 +      react {
    1.33 +        case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message)
    1.34 +        case bad => System.err.println("prover: ignoring bad message " + bad)
    1.35 +      }
    1.36 +    }
    1.37 +  }
    1.38 +}
    1.39 +
    1.40 +
    1.41 +object Command
    1.42 +{
    1.43 +  object Status extends Enumeration
    1.44 +  {
    1.45 +    val UNPROCESSED = Value("UNPROCESSED")
    1.46 +    val FINISHED = Value("FINISHED")
    1.47 +    val FAILED = Value("FAILED")
    1.48 +  }
    1.49 +
    1.50 +  case class HighlightInfo(highlight: String) { override def toString = highlight }
    1.51 +  case class TypeInfo(ty: String)
    1.52 +  case class RefInfo(file: Option[String], line: Option[Int],
    1.53 +    command_id: Option[String], offset: Option[Int])
    1.54 +}
    1.55 +
    1.56 +
    1.57 +class Command(
    1.58 +    val tokens: List[Token],
    1.59 +    val starts: Map[Token, Int]) extends Accumulator
    1.60 +{
    1.61 +  require(!tokens.isEmpty)
    1.62 +
    1.63 +  val id = Isabelle.system.id()
    1.64 +  override def hashCode = id.hashCode
    1.65 +
    1.66 +
    1.67 +  /* content */
    1.68 +
    1.69 +  override def toString = name
    1.70 +
    1.71 +  val name = tokens.head.content
    1.72 +  val content: String = Token.string_from_tokens(tokens, starts)
    1.73 +  def content(i: Int, j: Int): String = content.substring(i, j)
    1.74 +  val symbol_index = new Symbol.Index(content)
    1.75 +
    1.76 +  def start(doc: ProofDocument) = doc.token_start(tokens.first)
    1.77 +  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
    1.78 +
    1.79 +  def contains(p: Token) = tokens.contains(p)
    1.80 +
    1.81 +  protected override var _state = new State(this)
    1.82 +
    1.83 +
    1.84 +  /* markup */
    1.85 +
    1.86 +  lazy val empty_markup = new Markup_Text(Nil, content)
    1.87 +
    1.88 +  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
    1.89 +  {
    1.90 +    val start = symbol_index.decode(begin)
    1.91 +    val stop = symbol_index.decode(end)
    1.92 +    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
    1.93 +  }
    1.94 +
    1.95 +
    1.96 +  /* results, markup, ... */
    1.97 +
    1.98 +  private val empty_cmd_state = new Command_State(this)
    1.99 +  private def cmd_state(doc: ProofDocument) =
   1.100 +    doc.states.getOrElse(this, empty_cmd_state)
   1.101 +
   1.102 +  def status(doc: ProofDocument) = cmd_state(doc).state.status
   1.103 +  def results(doc: ProofDocument) = cmd_state(doc).results
   1.104 +  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
   1.105 +  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
   1.106 +  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
   1.107 +  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
   1.108 +}
   1.109 +
   1.110 +
   1.111 +class Command_State(val command: Command) extends Accumulator
   1.112 +{
   1.113 +  protected override var _state = new State(command)
   1.114 +
   1.115 +  def results: List[XML.Tree] =
   1.116 +    command.state.results ::: state.results
   1.117 +
   1.118 +  def markup_root: Markup_Text =
   1.119 +    (command.state.markup_root /: state.markup_root.markup)(_ + _)
   1.120 +
   1.121 +  def type_at(pos: Int): Option[String] = state.type_at(pos)
   1.122 +
   1.123 +  def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
   1.124 +
   1.125 +  def highlight: Markup_Text =
   1.126 +    (command.state.highlight /: state.highlight.markup)(_ + _)
   1.127 +}
   1.128 \ No newline at end of file