src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Tue Sep 07 23:59:14 2010 +0200 (2010-09-07)
changeset 39181 2257eded8323
parent 39178 83e9f3ccea9f
child 39182 cce0c10ed943
permissions -rw-r--r--
Document_View: select gutter message icons from markup over line range, not full range results;
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, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
    16 import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D}
    17 import javax.swing.{JPanel, ToolTipManager}
    18 import javax.swing.event.{CaretListener, CaretEvent}
    19 
    20 import org.gjt.sp.jedit.{jEdit, OperatingSystem}
    21 import org.gjt.sp.jedit.gui.RolloverButton
    22 import org.gjt.sp.jedit.options.GutterOptionPane
    23 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    24 import org.gjt.sp.jedit.syntax.SyntaxStyle
    25 
    26 
    27 object Document_View
    28 {
    29   /* document view of text area */
    30 
    31   private val key = new Object
    32 
    33   def init(model: Document_Model, text_area: TextArea): Document_View =
    34   {
    35     Swing_Thread.require()
    36     val doc_view = new Document_View(model, text_area)
    37     text_area.putClientProperty(key, doc_view)
    38     doc_view.activate()
    39     doc_view
    40   }
    41 
    42   def apply(text_area: TextArea): Option[Document_View] =
    43   {
    44     Swing_Thread.require()
    45     text_area.getClientProperty(key) match {
    46       case doc_view: Document_View => Some(doc_view)
    47       case _ => None
    48     }
    49   }
    50 
    51   def exit(text_area: TextArea)
    52   {
    53     Swing_Thread.require()
    54     apply(text_area) match {
    55       case None => error("No document view for text area: " + text_area)
    56       case Some(doc_view) =>
    57         doc_view.deactivate()
    58         text_area.putClientProperty(key, null)
    59     }
    60   }
    61 }
    62 
    63 
    64 class Document_View(val model: Document_Model, text_area: TextArea)
    65 {
    66   private val session = model.session
    67 
    68 
    69   /* extended token styles */
    70 
    71   private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
    72 
    73   def extend_styles()
    74   {
    75     Swing_Thread.require()
    76     styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
    77   }
    78   extend_styles()
    79 
    80   def set_styles()
    81   {
    82     Swing_Thread.require()
    83     text_area.getPainter.setStyles(styles)
    84   }
    85 
    86 
    87   /* visible line ranges */
    88 
    89   // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
    90   // NB: jEdit already normalizes \r\n and \r to \n
    91   def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
    92   {
    93     val stop = if (start < end) end - 1 else end min model.buffer.getLength
    94     Text.Range(start, stop)
    95   }
    96 
    97   def screen_lines_range(): Text.Range =
    98   {
    99     val start = text_area.getScreenLineStartOffset(0)
   100     val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
   101     proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
   102   }
   103 
   104   def invalidate_line_range(range: Text.Range)
   105   {
   106     text_area.invalidateLineRange(
   107       model.buffer.getLineOfOffset(range.start),
   108       model.buffer.getLineOfOffset(range.stop))
   109   }
   110 
   111 
   112   /* commands_changed_actor */
   113 
   114   private val commands_changed_actor = actor {
   115     loop {
   116       react {
   117         case Session.Commands_Changed(changed) =>
   118           val buffer = model.buffer
   119           Isabelle.swing_buffer_lock(buffer) {
   120             val snapshot = model.snapshot()
   121 
   122             if (changed.exists(snapshot.node.commands.contains))
   123               overview.repaint()
   124 
   125             val visible_range = screen_lines_range()
   126             val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
   127             if (visible_cmds.exists(changed)) {
   128               for {
   129                 line <- 0 until text_area.getVisibleLines
   130                 val start = text_area.getScreenLineStartOffset(line) if start >= 0
   131                 val end = text_area.getScreenLineEndOffset(line) if end >= 0
   132                 val range = proper_line_range(start, end)
   133                 val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   134                 if line_cmds.exists(changed)
   135               } text_area.invalidateScreenLineRange(line, line)
   136 
   137               // FIXME danger of deadlock!?
   138               // FIXME potentially slow!?
   139               model.buffer.propertiesChanged()
   140             }
   141           }
   142 
   143         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
   144       }
   145     }
   146   }
   147 
   148 
   149   /* subexpression highlighting */
   150 
   151   private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
   152     : Option[(Text.Range, Color)] =
   153   {
   154     val offset = text_area.xyToOffset(x, y)
   155     snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
   156       case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
   157       case _ => None
   158     }
   159   }
   160 
   161   private var highlight_range: Option[(Text.Range, Color)] = None
   162 
   163   private val focus_listener = new FocusAdapter {
   164     override def focusLost(e: FocusEvent) { highlight_range = None }
   165   }
   166 
   167   private val mouse_motion_listener = new MouseMotionAdapter {
   168     override def mouseMoved(e: MouseEvent) {
   169       val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
   170       if (!model.buffer.isLoaded) highlight_range = None
   171       else
   172         Isabelle.swing_buffer_lock(model.buffer) {
   173           highlight_range map { case (range, _) => invalidate_line_range(range) }
   174           highlight_range =
   175             if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
   176           highlight_range map { case (range, _) => invalidate_line_range(range) }
   177         }
   178     }
   179   }
   180 
   181 
   182   /* text_area_extension */
   183 
   184   private val text_area_extension = new TextAreaExtension
   185   {
   186     override def paintScreenLineRange(gfx: Graphics2D,
   187       first_line: Int, last_line: Int, physical_lines: Array[Int],
   188       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   189     {
   190       Isabelle.swing_buffer_lock(model.buffer) {
   191         val snapshot = model.snapshot()
   192         val saved_color = gfx.getColor
   193         val ascent = text_area.getPainter.getFontMetrics.getAscent
   194 
   195         try {
   196           for (i <- 0 until physical_lines.length) {
   197             if (physical_lines(i) != -1) {
   198               val line_range = proper_line_range(start(i), end(i))
   199 
   200               // background color: status
   201               val cmds = snapshot.node.command_range(snapshot.revert(line_range))
   202               for {
   203                 (command, command_start) <- cmds if !command.is_ignored
   204                 val range = line_range.restrict(snapshot.convert(command.range + command_start))
   205                 r <- Isabelle.gfx_range(text_area, range)
   206                 color <- Isabelle_Markup.status_color(snapshot, command)
   207               } {
   208                 gfx.setColor(color)
   209                 gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   210               }
   211 
   212               // background color: markup
   213               for {
   214                 Text.Info(range, Some(color)) <-
   215                   snapshot.select_markup(line_range)(Isabelle_Markup.background).iterator
   216                 r <- Isabelle.gfx_range(text_area, range)
   217               } {
   218                 gfx.setColor(color)
   219                 gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   220               }
   221 
   222               // sub-expression highlighting -- potentially from other snapshot
   223               highlight_range match {
   224                 case Some((range, color)) if line_range.overlaps(range) =>
   225                   Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   226                     case None =>
   227                     case Some(r) =>
   228                       gfx.setColor(color)
   229                       gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
   230                   }
   231                 case _ =>
   232               }
   233 
   234               // boxed text
   235               for {
   236                 Text.Info(range, Some(color)) <-
   237                   snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
   238                 r <- Isabelle.gfx_range(text_area, range)
   239               } {
   240                 gfx.setColor(color)
   241                 gfx.drawRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 3)
   242               }
   243 
   244               // squiggly underline
   245               for {
   246                 Text.Info(range, Some(color)) <-
   247                   snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   248                 r <- Isabelle.gfx_range(text_area, range)
   249               } {
   250                 gfx.setColor(color)
   251                 val x0 = (r.x / 2) * 2
   252                 val y0 = r.y + ascent + 1
   253                 for (x1 <- Range(x0, x0 + r.length, 2)) {
   254                   val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   255                   gfx.drawLine(x1, y1, x1 + 1, y1)
   256                 }
   257               }
   258             }
   259           }
   260         }
   261         finally { gfx.setColor(saved_color) }
   262       }
   263     }
   264 
   265     override def getToolTipText(x: Int, y: Int): String =
   266     {
   267       Isabelle.swing_buffer_lock(model.buffer) {
   268         val snapshot = model.snapshot()
   269         val offset = text_area.xyToOffset(x, y)
   270         snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
   271         {
   272           case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
   273           case _ => null
   274         }
   275       }
   276     }
   277   }
   278 
   279 
   280   /* gutter_extension */
   281 
   282   private val gutter_extension = new TextAreaExtension
   283   {
   284     override def paintScreenLineRange(gfx: Graphics2D,
   285       first_line: Int, last_line: Int, physical_lines: Array[Int],
   286       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   287     {
   288       val gutter = text_area.getGutter
   289       val width = GutterOptionPane.getSelectionAreaWidth
   290       val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
   291       val FOLD_MARKER_SIZE = 12
   292 
   293       if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
   294         Isabelle.swing_buffer_lock(model.buffer) {
   295           val snapshot = model.snapshot()
   296           for (i <- 0 until physical_lines.length) {
   297             if (physical_lines(i) != -1) {
   298               val line_range = proper_line_range(start(i), end(i))
   299 
   300               // gutter icons
   301               val icons =
   302                 (for (Text.Info(_, Some(icon)) <-
   303                   snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
   304                 yield icon).toList.sortWith(_ >= _)
   305               icons match {
   306                 case icon :: _ =>
   307                   val icn = icon.icon
   308                   val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
   309                   val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
   310                   icn.paintIcon(gutter, gfx, x0, y0)
   311                 case Nil =>
   312               }
   313             }
   314           }
   315         }
   316       }
   317     }
   318   }
   319 
   320 
   321   /* caret handling */
   322 
   323   def selected_command(): Option[Command] =
   324   {
   325     Swing_Thread.require()
   326     model.snapshot().node.proper_command_at(text_area.getCaretPosition)
   327   }
   328 
   329   private val caret_listener = new CaretListener {
   330     private val delay = Swing_Thread.delay_last(session.input_delay) {
   331       session.perspective.event(Session.Perspective)
   332     }
   333     override def caretUpdate(e: CaretEvent) { delay() }
   334   }
   335 
   336 
   337   /* overview of command status left of scrollbar */
   338 
   339   private val overview = new JPanel(new BorderLayout)
   340   {
   341     private val WIDTH = 10
   342     private val HEIGHT = 2
   343 
   344     setPreferredSize(new Dimension(WIDTH, 0))
   345 
   346     setRequestFocusEnabled(false)
   347 
   348     addMouseListener(new MouseAdapter {
   349       override def mousePressed(event: MouseEvent) {
   350         val line = y_to_line(event.getY)
   351         if (line >= 0 && line < text_area.getLineCount)
   352           text_area.setCaretPosition(text_area.getLineStartOffset(line))
   353       }
   354     })
   355 
   356     override def addNotify() {
   357       super.addNotify()
   358       ToolTipManager.sharedInstance.registerComponent(this)
   359     }
   360 
   361     override def removeNotify() {
   362       ToolTipManager.sharedInstance.unregisterComponent(this)
   363       super.removeNotify
   364     }
   365 
   366     override def getToolTipText(event: MouseEvent): String =
   367     {
   368       val line = y_to_line(event.getY())
   369       if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
   370       else ""
   371     }
   372 
   373     override def paintComponent(gfx: Graphics)
   374     {
   375       super.paintComponent(gfx)
   376       Swing_Thread.assert()
   377       val buffer = model.buffer
   378       Isabelle.buffer_lock(buffer) {
   379         val snapshot = model.snapshot()
   380         val saved_color = gfx.getColor  // FIXME needed!?
   381         try {
   382           for {
   383             (command, start) <- snapshot.node.command_starts
   384             if !command.is_ignored
   385             val line1 = buffer.getLineOfOffset(snapshot.convert(start))
   386             val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
   387             val y = line_to_y(line1)
   388             val height = HEIGHT * (line2 - line1)
   389             color <- Isabelle_Markup.overview_color(snapshot, command)
   390           } {
   391             gfx.setColor(color)
   392             gfx.fillRect(0, y, getWidth - 1, height)
   393           }
   394         }
   395         finally { gfx.setColor(saved_color) }
   396       }
   397     }
   398 
   399     private def line_to_y(line: Int): Int =
   400       (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
   401 
   402     private def y_to_line(y: Int): Int =
   403       (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
   404   }
   405 
   406 
   407   /* activation */
   408 
   409   private def activate()
   410   {
   411     text_area.getPainter.
   412       addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
   413     text_area.getGutter.addExtension(gutter_extension)
   414     text_area.addFocusListener(focus_listener)
   415     text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
   416     text_area.addCaretListener(caret_listener)
   417     text_area.addLeftOfScrollBar(overview)
   418     session.commands_changed += commands_changed_actor
   419   }
   420 
   421   private def deactivate()
   422   {
   423     session.commands_changed -= commands_changed_actor
   424     text_area.removeFocusListener(focus_listener)
   425     text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
   426     text_area.removeCaretListener(caret_listener)
   427     text_area.removeLeftOfScrollBar(overview)
   428     text_area.getGutter.removeExtension(gutter_extension)
   429     text_area.getPainter.removeExtension(text_area_extension)
   430   }
   431 }