src/Tools/jEdit/src/prover/Command.scala
author immler@in.tum.de
Thu Aug 27 10:51:09 2009 +0200 (2009-08-27 ago)
changeset 34676 9e725d34df7b
parent 34675 5427df0f6bcb
child 34688 1310dc269b4a
permissions -rw-r--r--
Command and Command_State handle results from prover as Accumulator
accumulating results in State;
prover outputs any result
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
immler@34674
    11
import scala.actors.Actor
immler@34674
    12
import scala.actors.Actor._
wenzelm@34318
    13
wenzelm@34497
    14
import scala.collection.mutable
wenzelm@34486
    15
immler@34662
    16
import isabelle.proofdocument.{Token, ProofDocument}
wenzelm@34451
    17
import isabelle.jedit.{Isabelle, Plugin}
wenzelm@34476
    18
import isabelle.XML
wenzelm@34451
    19
wenzelm@34451
    20
import sidekick.{SideKickParsedData, IAsset}
wenzelm@34451
    21
immler@34675
    22
trait Accumulator extends Actor
immler@34675
    23
{
immler@34675
    24
immler@34675
    25
  start() // start actor
immler@34675
    26
immler@34675
    27
  protected var _state: State
immler@34675
    28
  def state = _state
immler@34675
    29
immler@34675
    30
  override def act() {
immler@34675
    31
    loop {
immler@34675
    32
      react {
immler@34675
    33
        case x: XML.Tree => _state += x
immler@34675
    34
      }
immler@34675
    35
    }
immler@34675
    36
  }
immler@34675
    37
}
immler@34675
    38
wenzelm@34451
    39
wenzelm@34637
    40
object Command
wenzelm@34637
    41
{
wenzelm@34637
    42
  object Status extends Enumeration
wenzelm@34637
    43
  {
wenzelm@34318
    44
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    45
    val FINISHED = Value("FINISHED")
wenzelm@34318
    46
    val FAILED = Value("FAILED")
wenzelm@34318
    47
  }
wenzelm@34318
    48
}
wenzelm@34318
    49
wenzelm@34451
    50
immler@34674
    51
class Command(val tokens: List[Token], val starts: Map[Token, Int], chg_rec: Actor)
immler@34676
    52
extends Accumulator
wenzelm@34451
    53
{
wenzelm@34637
    54
  require(!tokens.isEmpty)
wenzelm@34637
    55
wenzelm@34603
    56
  val id = Isabelle.system.id()
immler@34653
    57
  override def hashCode = id.hashCode
wenzelm@34637
    58
immler@34674
    59
  def changed() = chg_rec ! this
immler@34674
    60
immler@34674
    61
wenzelm@34500
    62
  /* content */
wenzelm@34500
    63
wenzelm@34495
    64
  override def toString = name
wenzelm@34495
    65
immler@34526
    66
  val name = tokens.head.content
wenzelm@34582
    67
  val content: String = Token.string_from_tokens(tokens, starts)
wenzelm@34637
    68
  val symbol_index = new Symbol.Index(content)
wenzelm@34451
    69
immler@34554
    70
  def start(doc: ProofDocument) = doc.token_start(tokens.first)
immler@34554
    71
  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
wenzelm@34451
    72
immler@34593
    73
  def contains(p: Token) = tokens.contains(p)
immler@34593
    74
immler@34676
    75
  protected override var _state = State.empty(this)
immler@34676
    76
immler@34676
    77
immler@34676
    78
  /* markup */
wenzelm@34508
    79
immler@34676
    80
  lazy val empty_root_node =
immler@34676
    81
    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
immler@34676
    82
      Nil, id, content, RootInfo())
immler@34676
    83
immler@34676
    84
  def markup_node(begin: Int, end: Int, info: MarkupInfo) = {
immler@34676
    85
    new MarkupNode(this, symbol_index.decode(begin), symbol_index.decode(end), Nil, id,
immler@34676
    86
      content.substring(symbol_index.decode(begin), symbol_index.decode(end)),
immler@34676
    87
      info)
wenzelm@34500
    88
  }
wenzelm@34500
    89
immler@34676
    90
immler@34676
    91
  /* results, markup, ... */
wenzelm@34500
    92
immler@34676
    93
  private val empty_cmd_state = new Command_State(this)
immler@34676
    94
  private def cmd_state(doc: ProofDocument) =
immler@34676
    95
    doc.states.getOrElse(this, empty_cmd_state)
wenzelm@34500
    96
immler@34676
    97
  def status(doc: ProofDocument) = cmd_state(doc).state.status
immler@34676
    98
  def result_document(doc: ProofDocument) = cmd_state(doc).result_document
immler@34676
    99
  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
immler@34676
   100
  def highlight_node(doc: ProofDocument) = cmd_state(doc).highlight_node
immler@34676
   101
  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
immler@34676
   102
  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
immler@34676
   103
}
immler@34676
   104
wenzelm@34500
   105
immler@34676
   106
class Command_State(val cmd: Command)
immler@34676
   107
extends Accumulator
immler@34676
   108
{
immler@34676
   109
immler@34676
   110
  protected override var _state = State.empty(cmd)
immler@34676
   111
immler@34676
   112
immler@34676
   113
  // combining command and state
immler@34676
   114
  def result_document = {
immler@34676
   115
    val cmd_results = cmd.state.results
immler@34653
   116
    XML.document(
immler@34676
   117
      cmd_results.toList ::: state.results.toList match {
immler@34653
   118
        case Nil => XML.Elem("message", Nil, Nil)
immler@34653
   119
        case List(elem) => elem
immler@34653
   120
        case elems => XML.Elem("messages", Nil, elems)
immler@34653
   121
      }, "style")
immler@34653
   122
  }
wenzelm@34500
   123
immler@34676
   124
  def markup_root: MarkupNode = {
immler@34676
   125
    val cmd_markup_root = cmd.state.markup_root
immler@34676
   126
    (cmd_markup_root /: state.markup_root.children) (_ + _)
immler@34653
   127
  }
immler@34557
   128
immler@34676
   129
  def highlight_node: MarkupNode =
wenzelm@34637
   130
  {
immler@34560
   131
    import MarkupNode._
immler@34676
   132
    markup_root.filter(_.info match {
immler@34676
   133
      case RootInfo() | HighlightInfo(_) => true
immler@34560
   134
      case _ => false
immler@34560
   135
    }).head
immler@34560
   136
  }
immler@34556
   137
wenzelm@34637
   138
  def type_at(pos: Int): String =
wenzelm@34637
   139
  {
immler@34676
   140
    val types = state.markup_root.
immler@34676
   141
      filter(_.info match { case TypeInfo(_) => true case _ => false })
immler@34562
   142
    types.flatten(_.flatten).
immler@34676
   143
    find(t => t.start <= pos && t.stop > pos).
immler@34676
   144
    map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })).
immler@34676
   145
    getOrElse(null)
immler@34562
   146
  }
immler@34568
   147
immler@34568
   148
  def ref_at(pos: Int): Option[MarkupNode] =
immler@34676
   149
    state.markup_root.
immler@34676
   150
      filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
immler@34568
   151
      flatten(_.flatten).
immler@34568
   152
      find(t => t.start <= pos && t.stop > pos)
wenzelm@34451
   153
}