src/Tools/jEdit/src/proofdocument/command.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34769 826525fc5285
permissions -rw-r--r--
misc modernization of names;
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@34318
    12
wenzelm@34497
    13
import scala.collection.mutable
wenzelm@34486
    14
wenzelm@34451
    15
import isabelle.jedit.{Isabelle, Plugin}
wenzelm@34476
    16
import isabelle.XML
wenzelm@34451
    17
wenzelm@34451
    18
immler@34675
    19
trait Accumulator extends Actor
immler@34675
    20
{
immler@34675
    21
  start() // start actor
immler@34675
    22
immler@34675
    23
  protected var _state: State
immler@34675
    24
  def state = _state
immler@34675
    25
immler@34675
    26
  override def act() {
immler@34675
    27
    loop {
immler@34675
    28
      react {
wenzelm@34724
    29
        case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message)
wenzelm@34724
    30
        case bad => System.err.println("prover: ignoring bad message " + bad)
immler@34675
    31
      }
immler@34675
    32
    }
immler@34675
    33
  }
immler@34675
    34
}
immler@34675
    35
wenzelm@34451
    36
wenzelm@34637
    37
object Command
wenzelm@34637
    38
{
wenzelm@34637
    39
  object Status extends Enumeration
wenzelm@34637
    40
  {
wenzelm@34318
    41
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    42
    val FINISHED = Value("FINISHED")
wenzelm@34318
    43
    val FAILED = Value("FAILED")
wenzelm@34318
    44
  }
wenzelm@34707
    45
wenzelm@34707
    46
  case class HighlightInfo(highlight: String) { override def toString = highlight }
wenzelm@34717
    47
  case class TypeInfo(ty: String)
wenzelm@34707
    48
  case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@34717
    49
    command_id: Option[String], offset: Option[Int])
wenzelm@34318
    50
}
wenzelm@34318
    51
wenzelm@34451
    52
wenzelm@34697
    53
class Command(
wenzelm@34717
    54
    val tokens: List[Token],
wenzelm@34724
    55
    val starts: Map[Token, Int]) extends Accumulator
wenzelm@34451
    56
{
wenzelm@34637
    57
  require(!tokens.isEmpty)
wenzelm@34637
    58
wenzelm@34603
    59
  val id = Isabelle.system.id()
immler@34653
    60
  override def hashCode = id.hashCode
wenzelm@34637
    61
immler@34674
    62
wenzelm@34500
    63
  /* content */
wenzelm@34500
    64
wenzelm@34495
    65
  override def toString = name
wenzelm@34495
    66
immler@34526
    67
  val name = tokens.head.content
wenzelm@34582
    68
  val content: String = Token.string_from_tokens(tokens, starts)
wenzelm@34717
    69
  def content(i: Int, j: Int): String = content.substring(i, j)
wenzelm@34637
    70
  val symbol_index = new Symbol.Index(content)
wenzelm@34451
    71
wenzelm@34760
    72
  def start(doc: Proof_Document) = doc.token_start(tokens.first)
wenzelm@34760
    73
  def stop(doc: Proof_Document) = 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
wenzelm@34717
    82
  lazy val empty_markup = new Markup_Text(Nil, content)
immler@34676
    83
wenzelm@34717
    84
  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
wenzelm@34699
    85
  {
wenzelm@34703
    86
    val start = symbol_index.decode(begin)
wenzelm@34703
    87
    val stop = symbol_index.decode(end)
wenzelm@34717
    88
    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
wenzelm@34500
    89
  }
wenzelm@34500
    90
immler@34676
    91
immler@34676
    92
  /* results, markup, ... */
wenzelm@34500
    93
immler@34676
    94
  private val empty_cmd_state = new Command_State(this)
wenzelm@34760
    95
  private def cmd_state(doc: Proof_Document) =
immler@34676
    96
    doc.states.getOrElse(this, empty_cmd_state)
wenzelm@34500
    97
wenzelm@34760
    98
  def status(doc: Proof_Document) = cmd_state(doc).state.status
wenzelm@34760
    99
  def results(doc: Proof_Document) = cmd_state(doc).results
wenzelm@34760
   100
  def markup_root(doc: Proof_Document) = cmd_state(doc).markup_root
wenzelm@34760
   101
  def highlight(doc: Proof_Document) = cmd_state(doc).highlight
wenzelm@34760
   102
  def type_at(doc: Proof_Document, offset: Int) = cmd_state(doc).type_at(offset)
wenzelm@34760
   103
  def ref_at(doc: Proof_Document, offset: Int) = cmd_state(doc).ref_at(offset)
immler@34676
   104
}
immler@34676
   105
wenzelm@34500
   106
wenzelm@34698
   107
class Command_State(val command: Command) extends Accumulator
immler@34676
   108
{
wenzelm@34698
   109
  protected override var _state = new State(command)
immler@34676
   110
wenzelm@34746
   111
  def results: List[XML.Tree] =
wenzelm@34746
   112
    command.state.results ::: state.results
wenzelm@34500
   113
wenzelm@34717
   114
  def markup_root: Markup_Text =
wenzelm@34717
   115
    (command.state.markup_root /: state.markup_root.markup)(_ + _)
immler@34557
   116
wenzelm@34717
   117
  def type_at(pos: Int): Option[String] = state.type_at(pos)
immler@34556
   118
wenzelm@34717
   119
  def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
immler@34568
   120
wenzelm@34717
   121
  def highlight: Markup_Text =
wenzelm@34717
   122
    (command.state.highlight /: state.highlight.markup)(_ + _)
immler@34688
   123
}