src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Sun Sep 06 22:27:32 2009 +0200 (2009-09-06)
changeset 34717 3f32e08bbb6c
parent 34708 611864f2729d
child 34724 b1079c3ba1da
permissions -rw-r--r--
sidekick root data: set buffer length to avoid crash of initial caret move;
separate Markup_Node, Markup_Tree, Markup_Text;
added Markup_Text.flatten;
Command.type_at: null-free version;
eliminated Command.RootInfo;
simplified printing of TypeInfo, RefInfo;
added Command.content(Int, Int);
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
wenzelm@34699
    11
import scala.actors.Actor, Actor._
wenzelm@34318
    12
wenzelm@34497
    13
import scala.collection.mutable
wenzelm@34486
    14
immler@34662
    15
import isabelle.proofdocument.{Token, ProofDocument}
wenzelm@34451
    16
import isabelle.jedit.{Isabelle, Plugin}
wenzelm@34476
    17
import isabelle.XML
wenzelm@34451
    18
wenzelm@34451
    19
immler@34675
    20
trait Accumulator extends Actor
immler@34675
    21
{
immler@34675
    22
  start() // start actor
immler@34675
    23
immler@34675
    24
  protected var _state: State
immler@34675
    25
  def state = _state
immler@34675
    26
immler@34675
    27
  override def act() {
immler@34675
    28
    loop {
immler@34675
    29
      react {
wenzelm@34697
    30
        case message: XML.Tree => _state += message
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@34717
    55
    val starts: Map[Token, Int],
wenzelm@34697
    56
  change_receiver: Actor) extends Accumulator
wenzelm@34451
    57
{
wenzelm@34637
    58
  require(!tokens.isEmpty)
wenzelm@34637
    59
wenzelm@34603
    60
  val id = Isabelle.system.id()
immler@34653
    61
  override def hashCode = id.hashCode
wenzelm@34637
    62
wenzelm@34697
    63
  def changed() = change_receiver ! this
immler@34674
    64
immler@34674
    65
wenzelm@34500
    66
  /* content */
wenzelm@34500
    67
wenzelm@34495
    68
  override def toString = name
wenzelm@34495
    69
immler@34526
    70
  val name = tokens.head.content
wenzelm@34582
    71
  val content: String = Token.string_from_tokens(tokens, starts)
wenzelm@34717
    72
  def content(i: Int, j: Int): String = content.substring(i, j)
wenzelm@34637
    73
  val symbol_index = new Symbol.Index(content)
wenzelm@34451
    74
immler@34554
    75
  def start(doc: ProofDocument) = doc.token_start(tokens.first)
immler@34554
    76
  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
wenzelm@34451
    77
immler@34593
    78
  def contains(p: Token) = tokens.contains(p)
immler@34593
    79
wenzelm@34697
    80
  protected override var _state = new State(this)
immler@34676
    81
immler@34676
    82
immler@34676
    83
  /* markup */
wenzelm@34508
    84
wenzelm@34717
    85
  lazy val empty_markup = new Markup_Text(Nil, content)
immler@34676
    86
wenzelm@34717
    87
  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
wenzelm@34699
    88
  {
wenzelm@34703
    89
    val start = symbol_index.decode(begin)
wenzelm@34703
    90
    val stop = symbol_index.decode(end)
wenzelm@34717
    91
    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
wenzelm@34500
    92
  }
wenzelm@34500
    93
immler@34676
    94
immler@34676
    95
  /* results, markup, ... */
wenzelm@34500
    96
immler@34676
    97
  private val empty_cmd_state = new Command_State(this)
immler@34676
    98
  private def cmd_state(doc: ProofDocument) =
immler@34676
    99
    doc.states.getOrElse(this, empty_cmd_state)
wenzelm@34500
   100
immler@34676
   101
  def status(doc: ProofDocument) = cmd_state(doc).state.status
immler@34676
   102
  def result_document(doc: ProofDocument) = cmd_state(doc).result_document
immler@34676
   103
  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
wenzelm@34717
   104
  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
immler@34676
   105
  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
immler@34676
   106
  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
immler@34676
   107
}
immler@34676
   108
wenzelm@34500
   109
wenzelm@34698
   110
class Command_State(val command: Command) extends Accumulator
immler@34676
   111
{
wenzelm@34698
   112
  protected override var _state = new State(command)
immler@34676
   113
wenzelm@34698
   114
  def result_document: org.w3c.dom.Document =
immler@34653
   115
    XML.document(
wenzelm@34698
   116
      command.state.results ::: state.results match {
immler@34653
   117
        case Nil => XML.Elem("message", Nil, Nil)
immler@34653
   118
        case List(elem) => elem
immler@34653
   119
        case elems => XML.Elem("messages", Nil, elems)
immler@34653
   120
      }, "style")
wenzelm@34500
   121
wenzelm@34717
   122
  def markup_root: Markup_Text =
wenzelm@34717
   123
    (command.state.markup_root /: state.markup_root.markup)(_ + _)
immler@34557
   124
wenzelm@34717
   125
  def type_at(pos: Int): Option[String] = state.type_at(pos)
immler@34556
   126
wenzelm@34717
   127
  def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
immler@34568
   128
wenzelm@34717
   129
  def highlight: Markup_Text =
wenzelm@34717
   130
    (command.state.highlight /: state.highlight.markup)(_ + _)
immler@34688
   131
}