src/Tools/jEdit/src/proofdocument/command.scala
author wenzelm
Wed Dec 30 19:58:22 2009 +0100 (2009-12-30)
changeset 34815 6bae73cd8e33
parent 34813 f0107bc96961
child 34823 2f3ea37c5958
permissions -rw-r--r--
unified Command and Command_State, eliminated separate Accumulator;
Command.finish_static: idempotent transition from static to dynamic mode, taking snapshot of final state (which will never change later);
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@34760
     8
package isabelle.proofdocument
wenzelm@34318
     9
wenzelm@34451
    10
wenzelm@34699
    11
import scala.actors.Actor, Actor._
wenzelm@34497
    12
import scala.collection.mutable
wenzelm@34486
    13
wenzelm@34777
    14
import isabelle.jedit.Isabelle
immler@34675
    15
wenzelm@34451
    16
wenzelm@34637
    17
object Command
wenzelm@34637
    18
{
wenzelm@34637
    19
  object Status extends Enumeration
wenzelm@34637
    20
  {
wenzelm@34318
    21
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    22
    val FINISHED = Value("FINISHED")
wenzelm@34318
    23
    val FAILED = Value("FAILED")
wenzelm@34318
    24
  }
wenzelm@34707
    25
wenzelm@34707
    26
  case class HighlightInfo(highlight: String) { override def toString = highlight }
wenzelm@34717
    27
  case class TypeInfo(ty: String)
wenzelm@34707
    28
  case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@34717
    29
    command_id: Option[String], offset: Option[Int])
wenzelm@34318
    30
}
wenzelm@34318
    31
wenzelm@34451
    32
wenzelm@34697
    33
class Command(
wenzelm@34813
    34
    val id: Isar_Document.Command_ID,
wenzelm@34717
    35
    val tokens: List[Token],
wenzelm@34815
    36
    val starts: Map[Token, Int])
wenzelm@34815
    37
  extends Session.Entity
wenzelm@34451
    38
{
wenzelm@34637
    39
  require(!tokens.isEmpty)
wenzelm@34637
    40
wenzelm@34813
    41
  // FIXME override equality as well
immler@34653
    42
  override def hashCode = id.hashCode
wenzelm@34637
    43
immler@34674
    44
wenzelm@34500
    45
  /* content */
wenzelm@34500
    46
wenzelm@34495
    47
  override def toString = name
wenzelm@34495
    48
immler@34526
    49
  val name = tokens.head.content
wenzelm@34582
    50
  val content: String = Token.string_from_tokens(tokens, starts)
wenzelm@34717
    51
  def content(i: Int, j: Int): String = content.substring(i, j)
wenzelm@34637
    52
  val symbol_index = new Symbol.Index(content)
wenzelm@34451
    53
wenzelm@34760
    54
  def start(doc: Proof_Document) = doc.token_start(tokens.first)
wenzelm@34760
    55
  def stop(doc: Proof_Document) = doc.token_start(tokens.last) + tokens.last.length
wenzelm@34451
    56
immler@34593
    57
  def contains(p: Token) = tokens.contains(p)
immler@34593
    58
wenzelm@34815
    59
wenzelm@34815
    60
  /* accumulated messages */
wenzelm@34815
    61
wenzelm@34815
    62
  @volatile protected var state = new State(this)
wenzelm@34815
    63
  def current_state: State = state
wenzelm@34815
    64
wenzelm@34815
    65
  private case class Consume(session: Session, message: XML.Tree)
wenzelm@34815
    66
  private case object Finish
wenzelm@34815
    67
wenzelm@34815
    68
  private val accumulator = actor {
wenzelm@34815
    69
    var finished = false
wenzelm@34815
    70
    loop {
wenzelm@34815
    71
      react {
wenzelm@34815
    72
        case Consume(session: Session, message: XML.Tree) if !finished =>
wenzelm@34815
    73
          state = state.+(session, message)
wenzelm@34815
    74
wenzelm@34815
    75
        case Finish => finished = true; reply(())
wenzelm@34815
    76
wenzelm@34815
    77
        case bad => System.err.println("command accumulator: ignoring bad message " + bad)
wenzelm@34815
    78
      }
wenzelm@34815
    79
    }
wenzelm@34815
    80
  }
wenzelm@34815
    81
wenzelm@34815
    82
  def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
wenzelm@34815
    83
wenzelm@34815
    84
  def finish_static(state_id: Isar_Document.State_ID): Command =
wenzelm@34815
    85
  {
wenzelm@34815
    86
    val cmd = new Command(state_id, tokens, starts)
wenzelm@34815
    87
    accumulator !? Finish
wenzelm@34815
    88
    cmd.state = current_state
wenzelm@34815
    89
    cmd
wenzelm@34815
    90
  }
immler@34676
    91
immler@34676
    92
immler@34676
    93
  /* markup */
wenzelm@34508
    94
wenzelm@34717
    95
  lazy val empty_markup = new Markup_Text(Nil, content)
immler@34676
    96
wenzelm@34717
    97
  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
wenzelm@34699
    98
  {
wenzelm@34703
    99
    val start = symbol_index.decode(begin)
wenzelm@34703
   100
    val stop = symbol_index.decode(end)
wenzelm@34717
   101
    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
wenzelm@34500
   102
  }
wenzelm@34500
   103
immler@34676
   104
wenzelm@34815
   105
  /* results, markup, etc. */
wenzelm@34500
   106
wenzelm@34815
   107
  def results: List[XML.Tree] = current_state.results
wenzelm@34815
   108
  def markup_root: Markup_Text = current_state.markup_root
wenzelm@34815
   109
  def type_at(pos: Int): Option[String] = current_state.type_at(pos)
wenzelm@34815
   110
  def ref_at(pos: Int): Option[Markup_Node] = current_state.ref_at(pos)
wenzelm@34815
   111
  def highlight: Markup_Text = current_state.highlight
wenzelm@34500
   112
wenzelm@34815
   113
wenzelm@34815
   114
  private def cmd_state(doc: Proof_Document): State =  // FIXME clarify
wenzelm@34815
   115
    doc.states.getOrElse(this, this).current_state
wenzelm@34815
   116
wenzelm@34815
   117
  def status(doc: Proof_Document) = cmd_state(doc).status
wenzelm@34760
   118
  def results(doc: Proof_Document) = cmd_state(doc).results
wenzelm@34760
   119
  def markup_root(doc: Proof_Document) = cmd_state(doc).markup_root
wenzelm@34760
   120
  def highlight(doc: Proof_Document) = cmd_state(doc).highlight
wenzelm@34760
   121
  def type_at(doc: Proof_Document, offset: Int) = cmd_state(doc).type_at(offset)
wenzelm@34760
   122
  def ref_at(doc: Proof_Document, offset: Int) = cmd_state(doc).ref_at(offset)
immler@34676
   123
}