src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Sat May 29 20:34:28 2010 +0200 (2010-05-29)
changeset 37188 b78ff6b4f4b3
parent 37187 dc1927a0f534
child 37201 8517a650cfdc
permissions -rw-r--r--
do not highlight ignored command spans;
tuned;
     1 /*  Title:      Tools/jEdit/src/jedit/document_view.scala
     2     Author:     Fabian Immler, TU Munich
     3     Author:     Makarius
     4 
     5 Document view connected to jEdit text area.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import scala.actors.Actor._
    14 
    15 import java.awt.event.{MouseAdapter, MouseEvent}
    16 import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
    17 import javax.swing.{JPanel, ToolTipManager}
    18 import javax.swing.event.{CaretListener, CaretEvent}
    19 
    20 import org.gjt.sp.jedit.gui.RolloverButton
    21 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    22 
    23 
    24 object Document_View
    25 {
    26   def choose_color(document: Document, command: Command): Color =
    27   {
    28     val state = document.current_state(command)
    29     if (state.forks > 0) new Color(255, 228, 225)
    30     else if (state.forks < 0) Color.red
    31     else
    32       state.status match {
    33         case Command.Status.UNPROCESSED => new Color(255, 228, 225)
    34         case Command.Status.FINISHED => new Color(234, 248, 255)
    35         case Command.Status.FAILED => new Color(255, 193, 193)
    36         case Command.Status.UNDEFINED => Color.red
    37       }
    38   }
    39 
    40 
    41   /* document view of text area */
    42 
    43   private val key = new Object
    44 
    45   def init(model: Document_Model, text_area: TextArea): Document_View =
    46   {
    47     Swing_Thread.assert()
    48     val doc_view = new Document_View(model, text_area)
    49     text_area.putClientProperty(key, doc_view)
    50     doc_view.activate()
    51     doc_view
    52   }
    53 
    54   def apply(text_area: TextArea): Option[Document_View] =
    55   {
    56     Swing_Thread.assert()
    57     text_area.getClientProperty(key) match {
    58       case doc_view: Document_View => Some(doc_view)
    59       case _ => None
    60     }
    61   }
    62 
    63   def exit(text_area: TextArea)
    64   {
    65     Swing_Thread.assert()
    66     apply(text_area) match {
    67       case None => error("No document view for text area: " + text_area)
    68       case Some(doc_view) =>
    69         doc_view.deactivate()
    70         text_area.putClientProperty(key, null)
    71     }
    72   }
    73 }
    74 
    75 
    76 class Document_View(val model: Document_Model, text_area: TextArea)
    77 {
    78   private val session = model.session
    79 
    80 
    81   /* commands_changed_actor */
    82 
    83   private val commands_changed_actor = actor {
    84     loop {
    85       react {
    86         case Command_Set(changed) =>
    87           Swing_Thread.now {
    88             val document = model.recent_document()
    89             // FIXME cover doc states as well!!?
    90             for (command <- changed if document.commands.contains(command)) {
    91               update_syntax(document, command)
    92               invalidate_line(document, command)
    93               overview.repaint()
    94             }
    95           }
    96 
    97         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
    98       }
    99     }
   100   }
   101 
   102 
   103   /* text_area_extension */
   104 
   105   private val text_area_extension = new TextAreaExtension
   106   {
   107     override def paintValidLine(gfx: Graphics2D,
   108       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   109     {
   110       val document = model.recent_document()
   111       def from_current(pos: Int) = model.from_current(document, pos)
   112       def to_current(pos: Int) = model.to_current(document, pos)
   113       val metrics = text_area.getPainter.getFontMetrics
   114       val saved_color = gfx.getColor
   115       try {
   116         for ((command, command_start) <-
   117           document.command_range(from_current(start), from_current(end)) if !command.is_ignored)
   118         {
   119           val begin = start max to_current(command_start)
   120           val finish = (end - 1) min to_current(command_start + command.length)
   121           encolor(gfx, y, metrics.getHeight, begin, finish,
   122             Document_View.choose_color(document, command), true)
   123         }
   124       }
   125       finally { gfx.setColor(saved_color) }
   126     }
   127 
   128     override def getToolTipText(x: Int, y: Int): String =
   129     {
   130       val document = model.recent_document()
   131       val offset = model.from_current(document, text_area.xyToOffset(x, y))
   132       document.command_at(offset) match {
   133         case Some((command, command_start)) =>
   134           document.current_state(command).type_at(offset - command_start) getOrElse null
   135         case None => null
   136       }
   137     }
   138   }
   139 
   140 
   141   /* caret handling */
   142 
   143   def selected_command: Option[Command] =
   144     model.recent_document().command_at(text_area.getCaretPosition) match {
   145       case Some((command, _)) => Some(command)
   146       case None => None
   147     }
   148 
   149   private val caret_listener = new CaretListener
   150   {
   151     private var last_selected_command: Option[Command] = None
   152     override def caretUpdate(e: CaretEvent)
   153     {
   154       val selected = selected_command
   155       if (selected != last_selected_command) {
   156         last_selected_command = selected
   157         if (selected.isDefined) session.indicate_command_change(selected.get)
   158       }
   159     }
   160   }
   161 
   162 
   163   /* (re)painting */
   164 
   165   private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
   166   // FIXME update_delay property
   167 
   168   private def update_syntax(document: Document, cmd: Command)
   169   {
   170     val (line1, line2) = model.lines_of_command(document, cmd)
   171     if (line2 >= text_area.getFirstLine &&
   172       line1 <= text_area.getFirstLine + text_area.getVisibleLines)
   173         update_delay()
   174   }
   175 
   176   private def invalidate_line(document: Document, cmd: Command) =
   177   {
   178     val (start, stop) = model.lines_of_command(document, cmd)
   179     text_area.invalidateLineRange(start, stop)
   180   }
   181 
   182   private def invalidate_all() =
   183     text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
   184       text_area.getLastPhysicalLine)
   185 
   186   private def encolor(gfx: Graphics2D,
   187     y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
   188   {
   189     val start = text_area.offsetToXY(begin)
   190     val stop =
   191       if (finish < model.buffer.getLength) text_area.offsetToXY(finish)
   192       else {
   193         val p = text_area.offsetToXY(finish - 1)
   194         val metrics = text_area.getPainter.getFontMetrics
   195         p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
   196         p
   197       }
   198 
   199     if (start != null && stop != null) {
   200       gfx.setColor(color)
   201       if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
   202       else gfx.drawRect(start.x, y, stop.x - start.x, height)
   203     }
   204   }
   205 
   206 
   207   /* overview of command status left of scrollbar */
   208 
   209   private val overview = new JPanel(new BorderLayout)
   210   {
   211     private val WIDTH = 10
   212     private val HEIGHT = 2
   213 
   214     setPreferredSize(new Dimension(WIDTH, 0))
   215 
   216     setRequestFocusEnabled(false)
   217 
   218     addMouseListener(new MouseAdapter {
   219       override def mousePressed(event: MouseEvent) {
   220         val line = y_to_line(event.getY)
   221         if (line >= 0 && line < text_area.getLineCount)
   222           text_area.setCaretPosition(text_area.getLineStartOffset(line))
   223       }
   224     })
   225 
   226     override def addNotify() {
   227       super.addNotify()
   228       ToolTipManager.sharedInstance.registerComponent(this)
   229     }
   230 
   231     override def removeNotify() {
   232       ToolTipManager.sharedInstance.unregisterComponent(this)
   233       super.removeNotify
   234     }
   235 
   236     override def getToolTipText(event: MouseEvent): String =
   237     {
   238       val line = y_to_line(event.getY())
   239       if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
   240       else ""
   241     }
   242 
   243     override def paintComponent(gfx: Graphics)
   244     {
   245       super.paintComponent(gfx)
   246       val buffer = model.buffer
   247       val document = model.recent_document()
   248       def to_current(pos: Int) = model.to_current(document, pos)
   249       val saved_color = gfx.getColor
   250       try {
   251         for ((command, start) <- document.command_range(0) if !command.is_ignored) {
   252           val line1 = buffer.getLineOfOffset(to_current(start))
   253           val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
   254           val y = line_to_y(line1)
   255           val height = HEIGHT * (line2 - line1)
   256           gfx.setColor(Document_View.choose_color(document, command))
   257           gfx.fillRect(0, y, getWidth - 1, height)
   258         }
   259       }
   260       finally { gfx.setColor(saved_color) }
   261     }
   262 
   263     private def line_to_y(line: Int): Int =
   264       (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
   265 
   266     private def y_to_line(y: Int): Int =
   267       (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
   268   }
   269 
   270 
   271   /* activation */
   272 
   273   private def activate()
   274   {
   275     text_area.getPainter.
   276       addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
   277     text_area.addCaretListener(caret_listener)
   278     text_area.addLeftOfScrollBar(overview)
   279     session.commands_changed += commands_changed_actor
   280   }
   281 
   282   private def deactivate()
   283   {
   284     session.commands_changed -= commands_changed_actor
   285     text_area.removeLeftOfScrollBar(overview)
   286     text_area.removeCaretListener(caret_listener)
   287     text_area.getPainter.removeExtension(text_area_extension)
   288   }
   289 }