src/Tools/jEdit/src/proofdocument/theory_view.scala
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34772 1a79c9b9af82
     1.1 --- a/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 14:49:01 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 16:30:20 2009 +0100
     1.3 @@ -6,14 +6,12 @@
     1.4   * @author Makarius
     1.5   */
     1.6  
     1.7 -package isabelle.jedit
     1.8 +package isabelle.proofdocument
     1.9 +
    1.10  
    1.11  import scala.actors.Actor, Actor._
    1.12  import scala.collection.mutable
    1.13  
    1.14 -import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
    1.15 -import isabelle.prover.{Prover, Command}
    1.16 -
    1.17  import java.awt.{Color, Graphics2D}
    1.18  import javax.swing.event.{CaretListener, CaretEvent}
    1.19  
    1.20 @@ -21,10 +19,12 @@
    1.21  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
    1.22  import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
    1.23  
    1.24 +import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker, Raw_Output_Dockable}
    1.25  
    1.26 -object TheoryView
    1.27 +
    1.28 +object Theory_View
    1.29  {
    1.30 -  def choose_color(command: Command, doc: ProofDocument): Color =
    1.31 +  def choose_color(command: Command, doc: Proof_Document): Color =
    1.32    {
    1.33      command.status(doc) match {
    1.34        case Command.Status.UNPROCESSED => new Color(255, 228, 225)
    1.35 @@ -36,7 +36,7 @@
    1.36  }
    1.37  
    1.38  
    1.39 -class TheoryView(text_area: JEditTextArea)
    1.40 +class Theory_View(text_area: JEditTextArea)
    1.41  {
    1.42    private val buffer = text_area.getBuffer
    1.43  
    1.44 @@ -115,8 +115,8 @@
    1.45        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
    1.46      {
    1.47        val document = current_document()
    1.48 -      def from_current(pos: Int) = TheoryView.this.from_current(document, pos)
    1.49 -      def to_current(pos: Int) = TheoryView.this.to_current(document, pos)
    1.50 +      def from_current(pos: Int) = Theory_View.this.from_current(document, pos)
    1.51 +      def to_current(pos: Int) = Theory_View.this.to_current(document, pos)
    1.52        val saved_color = gfx.getColor
    1.53  
    1.54        val metrics = text_area.getPainter.getFontMetrics
    1.55 @@ -128,7 +128,7 @@
    1.56          val begin = start max to_current(e.start(document))
    1.57          val finish = (end - 1) min to_current(e.stop(document))
    1.58          encolor(gfx, y, metrics.getHeight, begin, finish,
    1.59 -          TheoryView.choose_color(e, document), true)
    1.60 +          Theory_View.choose_color(e, document), true)
    1.61          cmd = document.commands.next(e)
    1.62        }
    1.63  
    1.64 @@ -166,18 +166,19 @@
    1.65      }
    1.66    }
    1.67  
    1.68 -  def activate() {
    1.69 +  def activate()
    1.70 +  {
    1.71      text_area.addCaretListener(selected_state_controller)
    1.72      text_area.addLeftOfScrollBar(overview)
    1.73      text_area.getPainter.
    1.74        addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
    1.75 -    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
    1.76 +    buffer.setTokenMarker(new Isabelle_Token_Marker(buffer, prover))
    1.77      buffer.addBufferListener(buffer_listener)
    1.78  
    1.79      val dockable =
    1.80 -      text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
    1.81 +      text_area.getView.getDockableWindowManager.getDockable("isabelle-raw-output")
    1.82      if (dockable != null) {
    1.83 -      val output_dockable = dockable.asInstanceOf[OutputDockable]
    1.84 +      val output_dockable = dockable.asInstanceOf[Raw_Output_Dockable]
    1.85        val output_text_view = prover.output_text_view
    1.86        output_dockable.set_text(output_text_view)
    1.87      }
    1.88 @@ -196,7 +197,7 @@
    1.89  
    1.90    /* history of changes */
    1.91  
    1.92 -  private def doc_or_pred(c: Change): ProofDocument =
    1.93 +  private def doc_or_pred(c: Change): Proof_Document =
    1.94      prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
    1.95  
    1.96    def current_document() = doc_or_pred(current_change)
    1.97 @@ -254,14 +255,14 @@
    1.98  
    1.99    /* transforming offsets */
   1.100  
   1.101 -  private def changes_from(doc: ProofDocument): List[Edit] =
   1.102 +  private def changes_from(doc: Proof_Document): List[Edit] =
   1.103      List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
   1.104        edits.toList
   1.105  
   1.106 -  def from_current(doc: ProofDocument, offset: Int): Int =
   1.107 +  def from_current(doc: Proof_Document, offset: Int): Int =
   1.108      (offset /: changes_from(doc).reverse) ((i, change) => change before i)
   1.109  
   1.110 -  def to_current(doc: ProofDocument, offset: Int): Int =
   1.111 +  def to_current(doc: Proof_Document, offset: Int): Int =
   1.112      (offset /: changes_from(doc)) ((i, change) => change after i)
   1.113  
   1.114