src/Tools/jEdit/src/jedit/document_overview.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34777 91d6089cef88
permissions -rw-r--r--
misc modernization of names;
     1 /*
     2  * Information on command status left of scrollbar (with panel)
     3  *
     4  * @author Fabian Immler, TU Munich
     5  */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle.proofdocument.{Command, Proof_Document, Prover, Theory_View}
    11 
    12 import javax.swing.{JPanel, ToolTipManager}
    13 import java.awt.event.{MouseAdapter, MouseEvent}
    14 import java.awt.{BorderLayout, Graphics, Dimension}
    15 
    16 import org.gjt.sp.jedit.gui.RolloverButton
    17 import org.gjt.sp.jedit.textarea.JEditTextArea
    18 import org.gjt.sp.jedit.buffer.JEditBuffer
    19 
    20 
    21 class Document_Overview(
    22     prover: Prover,
    23     text_area: JEditTextArea,
    24     to_current: (Proof_Document, Int) => Int)
    25   extends JPanel(new BorderLayout)
    26 {
    27   private val WIDTH = 10
    28   private val HEIGHT = 2
    29 
    30   setRequestFocusEnabled(false)
    31 
    32   addMouseListener(new MouseAdapter {
    33     override def mousePressed(event: MouseEvent) {
    34       val line = y_to_line(event.getY)
    35       if (line >= 0 && line < text_area.getLineCount)
    36         text_area.setCaretPosition(text_area.getLineStartOffset(line))
    37     }
    38   })
    39 
    40   override def addNotify() {
    41     super.addNotify()
    42     ToolTipManager.sharedInstance.registerComponent(this)
    43   }
    44 
    45   override def removeNotify() {
    46     super.removeNotify
    47     ToolTipManager.sharedInstance.unregisterComponent(this)
    48   }
    49 
    50   override def getToolTipText(event: MouseEvent): String =
    51   {
    52     val buffer = text_area.getBuffer
    53     val lineCount = buffer.getLineCount
    54     val line = y_to_line(event.getY())
    55     if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
    56     else ""
    57   }
    58 
    59   override def paintComponent(gfx: Graphics) {
    60     super.paintComponent(gfx)
    61     val buffer = text_area.getBuffer
    62     val theory_view = Isabelle.prover_setup(buffer).get.theory_view
    63     val doc = theory_view.current_document()
    64 
    65     for (command <- doc.commands) {
    66       val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
    67       val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
    68       val y = line_to_y(line1)
    69       val height = HEIGHT * (line2 - line1)
    70       gfx.setColor(Theory_View.choose_color(command, doc))
    71       gfx.fillRect(0, y, getWidth - 1, height)
    72     }
    73   }
    74 
    75   override def getPreferredSize = new Dimension(WIDTH, 0)
    76 
    77   private def line_to_y(line: Int): Int =
    78     (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
    79 
    80   private def y_to_line(y: Int): Int =
    81     (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
    82 }