src/Tools/jEdit/src/proofdocument/command.scala
author wenzelm
Sun Jan 10 20:14:21 2010 +0100 (2010-01-10 ago)
changeset 34855 81d0410dc3ac
parent 34835 67733fd0e3fa
child 34856 aa9e22d9f9a7
permissions -rw-r--r--
iterators for ranges of commands/starts -- avoid extra array per document;
try/finally for saved_color;
misc tuning;
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@34832
    36
    val starts: Map[Token, Int])   // FIXME eliminate
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@34832
    52
  lazy val symbol_index = new Symbol.Index(content)
wenzelm@34451
    53
wenzelm@34855
    54
  def length: Int = content.length
wenzelm@34855
    55
wenzelm@34823
    56
  def start(doc: Document) = doc.token_start(tokens.first)
wenzelm@34855
    57
  def stop(doc: Document) = start(doc) + length
wenzelm@34451
    58
immler@34593
    59
  def contains(p: Token) = tokens.contains(p)
immler@34593
    60
wenzelm@34815
    61
wenzelm@34815
    62
  /* accumulated messages */
wenzelm@34815
    63
wenzelm@34815
    64
  @volatile protected var state = new State(this)
wenzelm@34815
    65
  def current_state: State = state
wenzelm@34815
    66
wenzelm@34815
    67
  private case class Consume(session: Session, message: XML.Tree)
wenzelm@34832
    68
  private case object Assign
wenzelm@34815
    69
wenzelm@34815
    70
  private val accumulator = actor {
wenzelm@34832
    71
    var assigned = false
wenzelm@34815
    72
    loop {
wenzelm@34815
    73
      react {
wenzelm@34832
    74
        case Consume(session: Session, message: XML.Tree) if !assigned =>
wenzelm@34815
    75
          state = state.+(session, message)
wenzelm@34815
    76
wenzelm@34832
    77
        case Assign =>
wenzelm@34835
    78
          assigned = true  // single assignment
wenzelm@34832
    79
          reply(())
wenzelm@34815
    80
wenzelm@34815
    81
        case bad => System.err.println("command accumulator: ignoring bad message " + bad)
wenzelm@34815
    82
      }
wenzelm@34815
    83
    }
wenzelm@34815
    84
  }
wenzelm@34815
    85
wenzelm@34815
    86
  def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
wenzelm@34815
    87
wenzelm@34832
    88
  def assign_state(state_id: Isar_Document.State_ID): Command =
wenzelm@34815
    89
  {
wenzelm@34815
    90
    val cmd = new Command(state_id, tokens, starts)
wenzelm@34832
    91
    accumulator !? Assign
wenzelm@34815
    92
    cmd.state = current_state
wenzelm@34815
    93
    cmd
wenzelm@34815
    94
  }
immler@34676
    95
immler@34676
    96
immler@34676
    97
  /* markup */
wenzelm@34508
    98
wenzelm@34717
    99
  lazy val empty_markup = new Markup_Text(Nil, content)
immler@34676
   100
wenzelm@34717
   101
  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
wenzelm@34699
   102
  {
wenzelm@34703
   103
    val start = symbol_index.decode(begin)
wenzelm@34703
   104
    val stop = symbol_index.decode(end)
wenzelm@34717
   105
    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
wenzelm@34500
   106
  }
immler@34676
   107
}