src/Tools/jEdit/src/prover/Command.scala
changeset 34759 bfea7839d9e1
parent 34758 710e3a9a4c95
child 34760 dc7f5e0d9d27
     1.1 --- a/src/Tools/jEdit/src/prover/Command.scala	Tue Dec 08 14:29:29 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,124 +0,0 @@
     1.4 -/*
     1.5 - * Prover commands with semantic state
     1.6 - *
     1.7 - * @author Johannes Hölzl, TU Munich
     1.8 - * @author Fabian Immler, TU Munich
     1.9 - */
    1.10 -
    1.11 -package isabelle.prover
    1.12 -
    1.13 -
    1.14 -import scala.actors.Actor, Actor._
    1.15 -
    1.16 -import scala.collection.mutable
    1.17 -
    1.18 -import isabelle.proofdocument.{Token, ProofDocument}
    1.19 -import isabelle.jedit.{Isabelle, Plugin}
    1.20 -import isabelle.XML
    1.21 -
    1.22 -
    1.23 -trait Accumulator extends Actor
    1.24 -{
    1.25 -  start() // start actor
    1.26 -
    1.27 -  protected var _state: State
    1.28 -  def state = _state
    1.29 -
    1.30 -  override def act() {
    1.31 -    loop {
    1.32 -      react {
    1.33 -        case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message)
    1.34 -        case bad => System.err.println("prover: ignoring bad message " + bad)
    1.35 -      }
    1.36 -    }
    1.37 -  }
    1.38 -}
    1.39 -
    1.40 -
    1.41 -object Command
    1.42 -{
    1.43 -  object Status extends Enumeration
    1.44 -  {
    1.45 -    val UNPROCESSED = Value("UNPROCESSED")
    1.46 -    val FINISHED = Value("FINISHED")
    1.47 -    val FAILED = Value("FAILED")
    1.48 -  }
    1.49 -
    1.50 -  case class HighlightInfo(highlight: String) { override def toString = highlight }
    1.51 -  case class TypeInfo(ty: String)
    1.52 -  case class RefInfo(file: Option[String], line: Option[Int],
    1.53 -    command_id: Option[String], offset: Option[Int])
    1.54 -}
    1.55 -
    1.56 -
    1.57 -class Command(
    1.58 -    val tokens: List[Token],
    1.59 -    val starts: Map[Token, Int]) extends Accumulator
    1.60 -{
    1.61 -  require(!tokens.isEmpty)
    1.62 -
    1.63 -  val id = Isabelle.system.id()
    1.64 -  override def hashCode = id.hashCode
    1.65 -
    1.66 -
    1.67 -  /* content */
    1.68 -
    1.69 -  override def toString = name
    1.70 -
    1.71 -  val name = tokens.head.content
    1.72 -  val content: String = Token.string_from_tokens(tokens, starts)
    1.73 -  def content(i: Int, j: Int): String = content.substring(i, j)
    1.74 -  val symbol_index = new Symbol.Index(content)
    1.75 -
    1.76 -  def start(doc: ProofDocument) = doc.token_start(tokens.first)
    1.77 -  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
    1.78 -
    1.79 -  def contains(p: Token) = tokens.contains(p)
    1.80 -
    1.81 -  protected override var _state = new State(this)
    1.82 -
    1.83 -
    1.84 -  /* markup */
    1.85 -
    1.86 -  lazy val empty_markup = new Markup_Text(Nil, content)
    1.87 -
    1.88 -  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
    1.89 -  {
    1.90 -    val start = symbol_index.decode(begin)
    1.91 -    val stop = symbol_index.decode(end)
    1.92 -    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
    1.93 -  }
    1.94 -
    1.95 -
    1.96 -  /* results, markup, ... */
    1.97 -
    1.98 -  private val empty_cmd_state = new Command_State(this)
    1.99 -  private def cmd_state(doc: ProofDocument) =
   1.100 -    doc.states.getOrElse(this, empty_cmd_state)
   1.101 -
   1.102 -  def status(doc: ProofDocument) = cmd_state(doc).state.status
   1.103 -  def results(doc: ProofDocument) = cmd_state(doc).results
   1.104 -  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
   1.105 -  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
   1.106 -  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
   1.107 -  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
   1.108 -}
   1.109 -
   1.110 -
   1.111 -class Command_State(val command: Command) extends Accumulator
   1.112 -{
   1.113 -  protected override var _state = new State(command)
   1.114 -
   1.115 -  def results: List[XML.Tree] =
   1.116 -    command.state.results ::: state.results
   1.117 -
   1.118 -  def markup_root: Markup_Text =
   1.119 -    (command.state.markup_root /: state.markup_root.markup)(_ + _)
   1.120 -
   1.121 -  def type_at(pos: Int): Option[String] = state.type_at(pos)
   1.122 -
   1.123 -  def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
   1.124 -
   1.125 -  def highlight: Markup_Text =
   1.126 -    (command.state.highlight /: state.highlight.markup)(_ + _)
   1.127 -}
   1.128 \ No newline at end of file