src/Tools/jEdit/src/proofdocument/command.scala
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34769 826525fc5285
     1.1 --- a/src/Tools/jEdit/src/proofdocument/command.scala	Tue Dec 08 14:49:01 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala	Tue Dec 08 16:30:20 2009 +0100
     1.3 @@ -5,14 +5,13 @@
     1.4   * @author Fabian Immler, TU Munich
     1.5   */
     1.6  
     1.7 -package isabelle.prover
     1.8 +package isabelle.proofdocument
     1.9  
    1.10  
    1.11  import scala.actors.Actor, Actor._
    1.12  
    1.13  import scala.collection.mutable
    1.14  
    1.15 -import isabelle.proofdocument.{Token, ProofDocument}
    1.16  import isabelle.jedit.{Isabelle, Plugin}
    1.17  import isabelle.XML
    1.18  
    1.19 @@ -70,8 +69,8 @@
    1.20    def content(i: Int, j: Int): String = content.substring(i, j)
    1.21    val symbol_index = new Symbol.Index(content)
    1.22  
    1.23 -  def start(doc: ProofDocument) = doc.token_start(tokens.first)
    1.24 -  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
    1.25 +  def start(doc: Proof_Document) = doc.token_start(tokens.first)
    1.26 +  def stop(doc: Proof_Document) = doc.token_start(tokens.last) + tokens.last.length
    1.27  
    1.28    def contains(p: Token) = tokens.contains(p)
    1.29  
    1.30 @@ -93,15 +92,15 @@
    1.31    /* results, markup, ... */
    1.32  
    1.33    private val empty_cmd_state = new Command_State(this)
    1.34 -  private def cmd_state(doc: ProofDocument) =
    1.35 +  private def cmd_state(doc: Proof_Document) =
    1.36      doc.states.getOrElse(this, empty_cmd_state)
    1.37  
    1.38 -  def status(doc: ProofDocument) = cmd_state(doc).state.status
    1.39 -  def results(doc: ProofDocument) = cmd_state(doc).results
    1.40 -  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
    1.41 -  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
    1.42 -  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
    1.43 -  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
    1.44 +  def status(doc: Proof_Document) = cmd_state(doc).state.status
    1.45 +  def results(doc: Proof_Document) = cmd_state(doc).results
    1.46 +  def markup_root(doc: Proof_Document) = cmd_state(doc).markup_root
    1.47 +  def highlight(doc: Proof_Document) = cmd_state(doc).highlight
    1.48 +  def type_at(doc: Proof_Document, offset: Int) = cmd_state(doc).type_at(offset)
    1.49 +  def ref_at(doc: Proof_Document, offset: Int) = cmd_state(doc).ref_at(offset)
    1.50  }
    1.51  
    1.52