src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Sat Sep 04 22:00:25 2010 +0200 (2010-09-04)
changeset 39131 947c62440026
parent 39044 5c13736e81c7
child 39132 ba17ca3acdd3
permissions -rw-r--r--
basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm@36760
     1
/*  Title:      Tools/jEdit/src/jedit/document_view.scala
wenzelm@36760
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36760
     3
    Author:     Makarius
wenzelm@36760
     4
wenzelm@36760
     5
Document view connected to jEdit text area.
wenzelm@36760
     6
*/
wenzelm@34408
     7
immler@34403
     8
package isabelle.jedit
immler@34403
     9
wenzelm@34760
    10
wenzelm@36015
    11
import isabelle._
wenzelm@36015
    12
wenzelm@34784
    13
import scala.actors.Actor._
wenzelm@34784
    14
wenzelm@39131
    15
import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
wenzelm@34784
    16
import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
wenzelm@34734
    17
import javax.swing.{JPanel, ToolTipManager}
wenzelm@34784
    18
import javax.swing.event.{CaretListener, CaretEvent}
wenzelm@34734
    19
wenzelm@39131
    20
import org.gjt.sp.jedit.OperatingSystem
wenzelm@34709
    21
import org.gjt.sp.jedit.gui.RolloverButton
wenzelm@34784
    22
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
wenzelm@37241
    23
import org.gjt.sp.jedit.syntax.SyntaxStyle
wenzelm@34784
    24
wenzelm@34784
    25
wenzelm@34784
    26
object Document_View
wenzelm@34784
    27
{
wenzelm@39044
    28
  /* physical rendering */
wenzelm@39044
    29
wenzelm@39044
    30
  def status_color(snapshot: Document.Snapshot, command: Command): Color =
wenzelm@34784
    31
  {
wenzelm@38356
    32
    val state = snapshot.state(command)
wenzelm@38151
    33
    if (snapshot.is_outdated) new Color(240, 240, 240)
wenzelm@37186
    34
    else
wenzelm@38567
    35
      Isar_Document.command_status(state.status) match {
wenzelm@38567
    36
        case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
wenzelm@38567
    37
        case Isar_Document.Finished => new Color(234, 248, 255)
wenzelm@38567
    38
        case Isar_Document.Failed => new Color(255, 193, 193)
wenzelm@38567
    39
        case Isar_Document.Unprocessed => new Color(255, 228, 225)
wenzelm@38429
    40
        case _ => Color.red
wenzelm@37186
    41
      }
wenzelm@34784
    42
  }
wenzelm@34784
    43
wenzelm@39044
    44
  val message_markup: PartialFunction[Text.Info[Any], Color] =
wenzelm@39044
    45
  {
wenzelm@39044
    46
    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(220, 220, 220)
wenzelm@39044
    47
    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => new Color(255, 165, 0)
wenzelm@39044
    48
    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => new Color(255, 106, 106)
wenzelm@39044
    49
  }
wenzelm@39044
    50
wenzelm@34784
    51
wenzelm@34784
    52
  /* document view of text area */
wenzelm@34784
    53
wenzelm@34784
    54
  private val key = new Object
wenzelm@34784
    55
wenzelm@34784
    56
  def init(model: Document_Model, text_area: TextArea): Document_View =
wenzelm@34784
    57
  {
wenzelm@38223
    58
    Swing_Thread.require()
wenzelm@34784
    59
    val doc_view = new Document_View(model, text_area)
wenzelm@34784
    60
    text_area.putClientProperty(key, doc_view)
wenzelm@34784
    61
    doc_view.activate()
wenzelm@34784
    62
    doc_view
wenzelm@34784
    63
  }
wenzelm@34784
    64
wenzelm@34788
    65
  def apply(text_area: TextArea): Option[Document_View] =
wenzelm@34784
    66
  {
wenzelm@38223
    67
    Swing_Thread.require()
wenzelm@34784
    68
    text_area.getClientProperty(key) match {
wenzelm@34784
    69
      case doc_view: Document_View => Some(doc_view)
wenzelm@34784
    70
      case _ => None
wenzelm@34784
    71
    }
wenzelm@34784
    72
  }
wenzelm@34784
    73
wenzelm@34784
    74
  def exit(text_area: TextArea)
wenzelm@34784
    75
  {
wenzelm@38223
    76
    Swing_Thread.require()
wenzelm@34788
    77
    apply(text_area) match {
wenzelm@34784
    78
      case None => error("No document view for text area: " + text_area)
wenzelm@34784
    79
      case Some(doc_view) =>
wenzelm@34784
    80
        doc_view.deactivate()
wenzelm@34784
    81
        text_area.putClientProperty(key, null)
wenzelm@34784
    82
    }
wenzelm@34784
    83
  }
wenzelm@34784
    84
}
immler@34403
    85
wenzelm@34733
    86
wenzelm@37129
    87
class Document_View(val model: Document_Model, text_area: TextArea)
immler@34654
    88
{
wenzelm@34784
    89
  private val session = model.session
wenzelm@34784
    90
immler@34403
    91
wenzelm@37241
    92
  /* extended token styles */
wenzelm@37241
    93
wenzelm@37241
    94
  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
wenzelm@37241
    95
wenzelm@37241
    96
  def extend_styles()
wenzelm@37241
    97
  {
wenzelm@38223
    98
    Swing_Thread.require()
wenzelm@38158
    99
    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
wenzelm@37241
   100
  }
wenzelm@37241
   101
  extend_styles()
wenzelm@37241
   102
wenzelm@37241
   103
  def set_styles()
wenzelm@37241
   104
  {
wenzelm@38223
   105
    Swing_Thread.require()
wenzelm@37241
   106
    text_area.getPainter.setStyles(styles)
wenzelm@37241
   107
  }
wenzelm@37241
   108
wenzelm@37241
   109
wenzelm@38881
   110
  /* visible line ranges */
wenzelm@38881
   111
wenzelm@38883
   112
  // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
wenzelm@38881
   113
  // NB: jEdit already normalizes \r\n and \r to \n
wenzelm@38881
   114
  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
wenzelm@38881
   115
  {
wenzelm@38883
   116
    val stop = if (start < end) end - 1 else end min model.buffer.getLength
wenzelm@38881
   117
    Text.Range(start, stop)
wenzelm@38881
   118
  }
wenzelm@38881
   119
wenzelm@38881
   120
  def screen_lines_range(): Text.Range =
wenzelm@38881
   121
  {
wenzelm@38881
   122
    val start = text_area.getScreenLineStartOffset(0)
wenzelm@38881
   123
    val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
wenzelm@38881
   124
    proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
wenzelm@38881
   125
  }
wenzelm@38881
   126
wenzelm@38881
   127
wenzelm@37129
   128
  /* commands_changed_actor */
wenzelm@34834
   129
wenzelm@37129
   130
  private val commands_changed_actor = actor {
wenzelm@34784
   131
    loop {
wenzelm@34784
   132
      react {
wenzelm@38360
   133
        case Session.Commands_Changed(changed) =>
wenzelm@38843
   134
          val buffer = model.buffer
wenzelm@38843
   135
          Isabelle.swing_buffer_lock(buffer) {
wenzelm@38151
   136
            val snapshot = model.snapshot()
wenzelm@38881
   137
wenzelm@38884
   138
            if (changed.exists(snapshot.node.commands.contains))
wenzelm@38884
   139
              overview.repaint()
wenzelm@38884
   140
wenzelm@38881
   141
            val visible_range = screen_lines_range()
wenzelm@38881
   142
            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
wenzelm@38881
   143
            if (visible_cmds.exists(changed)) {
wenzelm@38881
   144
              for {
wenzelm@38881
   145
                line <- 0 until text_area.getVisibleLines
wenzelm@38881
   146
                val start = text_area.getScreenLineStartOffset(line) if start >= 0
wenzelm@38881
   147
                val end = text_area.getScreenLineEndOffset(line) if end >= 0
wenzelm@38881
   148
                val range = proper_line_range(start, end)
wenzelm@38881
   149
                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
wenzelm@38881
   150
                if line_cmds.exists(changed)
wenzelm@38881
   151
              } text_area.invalidateScreenLineRange(line, line)
wenzelm@38884
   152
wenzelm@38843
   153
              // FIXME danger of deadlock!?
wenzelm@38881
   154
              // FIXME potentially slow!?
wenzelm@38881
   155
              model.buffer.propertiesChanged()
wenzelm@38640
   156
            }
wenzelm@34834
   157
          }
wenzelm@34784
   158
wenzelm@34784
   159
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@34784
   160
      }
immler@34403
   161
    }
immler@34678
   162
  }
immler@34403
   163
immler@34403
   164
wenzelm@39131
   165
  /* subexpression highlighting */
wenzelm@39131
   166
wenzelm@39131
   167
  private var highlight_point: Option[(Int, Int)] = None
wenzelm@39131
   168
wenzelm@39131
   169
  private val focus_listener = new FocusAdapter {
wenzelm@39131
   170
    override def focusLost(e: FocusEvent) { highlight_point = None }
wenzelm@39131
   171
  }
wenzelm@39131
   172
wenzelm@39131
   173
  private val mouse_motion_listener = new MouseMotionAdapter {
wenzelm@39131
   174
    override def mouseMoved(e: MouseEvent) {
wenzelm@39131
   175
      val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
wenzelm@39131
   176
      def refresh()
wenzelm@39131
   177
      {
wenzelm@39131
   178
        val offset = text_area.xyToOffset(e.getX(), e.getY())
wenzelm@39131
   179
        text_area.invalidateLine(model.buffer.getLineOfOffset(offset))
wenzelm@39131
   180
      }
wenzelm@39131
   181
      if (!model.buffer.isLoaded) highlight_point = None
wenzelm@39131
   182
      else if (!control) { highlight_point = None; refresh() }
wenzelm@39131
   183
      else { highlight_point = Some((e.getX(), e.getY())); refresh() }
wenzelm@39131
   184
    }
wenzelm@39131
   185
  }
wenzelm@39131
   186
wenzelm@39131
   187
wenzelm@34784
   188
  /* text_area_extension */
wenzelm@34784
   189
wenzelm@34784
   190
  private val text_area_extension = new TextAreaExtension
immler@34678
   191
  {
wenzelm@37685
   192
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@37685
   193
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@38886
   194
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@34784
   195
    {
wenzelm@38843
   196
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38843
   197
        val snapshot = model.snapshot()
wenzelm@38843
   198
        val saved_color = gfx.getColor
wenzelm@39044
   199
        val ascent = text_area.getPainter.getFontMetrics.getAscent
wenzelm@39131
   200
wenzelm@39131
   201
        // subexpression markup
wenzelm@39131
   202
        val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
wenzelm@39131
   203
        {
wenzelm@39131
   204
          case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) => Some(range)
wenzelm@39131
   205
        }
wenzelm@39131
   206
        val subexp_range: Option[Text.Range] =
wenzelm@39131
   207
          highlight_point match {
wenzelm@39131
   208
            case Some((x, y)) =>
wenzelm@39131
   209
              val offset = text_area.xyToOffset(x, y)
wenzelm@39131
   210
              val markup =
wenzelm@39131
   211
                snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
wenzelm@39131
   212
              if (markup.hasNext) markup.next.info else None
wenzelm@39131
   213
            case None => None
wenzelm@39131
   214
          }
wenzelm@39131
   215
wenzelm@38843
   216
        try {
wenzelm@38843
   217
          for (i <- 0 until physical_lines.length) {
wenzelm@38843
   218
            if (physical_lines(i) != -1) {
wenzelm@38881
   219
              val line_range = proper_line_range(start(i), end(i))
wenzelm@39044
   220
wenzelm@39044
   221
              // background color
wenzelm@38880
   222
              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
wenzelm@39044
   223
              for {
wenzelm@39044
   224
                (command, command_start) <- cmds if !command.is_ignored
wenzelm@38880
   225
                val range = line_range.restrict(snapshot.convert(command.range + command_start))
wenzelm@39044
   226
                r <- Isabelle.gfx_range(text_area, range)
wenzelm@39044
   227
              } {
wenzelm@39044
   228
                gfx.setColor(Document_View.status_color(snapshot, command))
wenzelm@39044
   229
                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@39044
   230
              }
wenzelm@39044
   231
wenzelm@39131
   232
              // subexpression highlighting
wenzelm@39131
   233
              if (subexp_range.isDefined) {
wenzelm@39131
   234
                val range = snapshot.convert(subexp_range.get)
wenzelm@39131
   235
                if (line_range.overlaps(range)) {
wenzelm@39131
   236
                  Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
wenzelm@39131
   237
                    case None =>
wenzelm@39131
   238
                    case Some(r) =>
wenzelm@39131
   239
                      gfx.setColor(Color.black)
wenzelm@39131
   240
                      gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
wenzelm@39131
   241
                  }
wenzelm@39131
   242
                }
wenzelm@39131
   243
              }
wenzelm@39131
   244
wenzelm@39044
   245
              // squiggly underline
wenzelm@39044
   246
              for {
wenzelm@39044
   247
                Text.Info(range, color) <-
wenzelm@39044
   248
                  snapshot.select_markup(line_range)(Document_View.message_markup)(null)
wenzelm@39044
   249
                if color != null
wenzelm@39044
   250
                r <- Isabelle.gfx_range(text_area, range)
wenzelm@39044
   251
              } {
wenzelm@39044
   252
                gfx.setColor(color)
wenzelm@39044
   253
                val x0 = (r.x / 2) * 2
wenzelm@39044
   254
                val y0 = r.y + ascent + 1
wenzelm@39044
   255
                for (x1 <- Range(x0, x0 + r.length, 2)) {
wenzelm@39044
   256
                  val y1 = if (x1 % 4 < 2) y0 else y0 + 1
wenzelm@39044
   257
                  gfx.drawLine(x1, y1, x1 + 1, y1)
wenzelm@38883
   258
                }
wenzelm@38843
   259
              }
wenzelm@38843
   260
            }
wenzelm@38223
   261
          }
wenzelm@38223
   262
        }
wenzelm@38843
   263
        finally { gfx.setColor(saved_color) }
wenzelm@38223
   264
      }
wenzelm@34784
   265
    }
wenzelm@34784
   266
wenzelm@34784
   267
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   268
    {
wenzelm@38845
   269
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38845
   270
        val snapshot = model.snapshot()
wenzelm@38845
   271
        val offset = text_area.xyToOffset(x, y)
wenzelm@38845
   272
        val markup =
wenzelm@38845
   273
          snapshot.select_markup(Text.Range(offset, offset + 1)) {
wenzelm@38580
   274
            case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@38845
   275
              Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
wenzelm@38845
   276
          } { null }
wenzelm@38845
   277
        if (markup.hasNext) markup.next.info else null
wenzelm@34784
   278
      }
wenzelm@34734
   279
    }
immler@34678
   280
  }
immler@34513
   281
wenzelm@34784
   282
wenzelm@37129
   283
  /* caret handling */
wenzelm@34810
   284
wenzelm@37849
   285
  def selected_command(): Option[Command] =
wenzelm@38223
   286
  {
wenzelm@38223
   287
    Swing_Thread.require()
wenzelm@38151
   288
    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
wenzelm@38223
   289
  }
wenzelm@34810
   290
wenzelm@37849
   291
  private val caret_listener = new CaretListener {
wenzelm@37849
   292
    private val delay = Swing_Thread.delay_last(session.input_delay) {
wenzelm@37849
   293
      session.perspective.event(Session.Perspective)
wenzelm@34810
   294
    }
wenzelm@37849
   295
    override def caretUpdate(e: CaretEvent) { delay() }
wenzelm@34810
   296
  }
wenzelm@34810
   297
wenzelm@34810
   298
wenzelm@34784
   299
  /* overview of command status left of scrollbar */
wenzelm@34784
   300
wenzelm@34834
   301
  private val overview = new JPanel(new BorderLayout)
wenzelm@34784
   302
  {
wenzelm@34784
   303
    private val WIDTH = 10
wenzelm@34784
   304
    private val HEIGHT = 2
wenzelm@34784
   305
wenzelm@34806
   306
    setPreferredSize(new Dimension(WIDTH, 0))
wenzelm@34806
   307
wenzelm@34784
   308
    setRequestFocusEnabled(false)
wenzelm@34784
   309
wenzelm@34784
   310
    addMouseListener(new MouseAdapter {
wenzelm@34784
   311
      override def mousePressed(event: MouseEvent) {
wenzelm@34784
   312
        val line = y_to_line(event.getY)
wenzelm@34784
   313
        if (line >= 0 && line < text_area.getLineCount)
wenzelm@34784
   314
          text_area.setCaretPosition(text_area.getLineStartOffset(line))
wenzelm@34784
   315
      }
wenzelm@34784
   316
    })
wenzelm@34784
   317
wenzelm@34784
   318
    override def addNotify() {
wenzelm@34784
   319
      super.addNotify()
wenzelm@34784
   320
      ToolTipManager.sharedInstance.registerComponent(this)
wenzelm@34784
   321
    }
immler@34403
   322
wenzelm@34784
   323
    override def removeNotify() {
wenzelm@34784
   324
      ToolTipManager.sharedInstance.unregisterComponent(this)
wenzelm@34784
   325
      super.removeNotify
wenzelm@34784
   326
    }
wenzelm@34784
   327
wenzelm@34784
   328
    override def getToolTipText(event: MouseEvent): String =
wenzelm@34784
   329
    {
wenzelm@34784
   330
      val line = y_to_line(event.getY())
wenzelm@34784
   331
      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
wenzelm@34784
   332
      else ""
wenzelm@34784
   333
    }
wenzelm@34784
   334
wenzelm@34784
   335
    override def paintComponent(gfx: Graphics)
wenzelm@34784
   336
    {
wenzelm@34784
   337
      super.paintComponent(gfx)
wenzelm@38640
   338
      Swing_Thread.assert()
wenzelm@34784
   339
      val buffer = model.buffer
wenzelm@38843
   340
      Isabelle.buffer_lock(buffer) {
wenzelm@38640
   341
        val snapshot = model.snapshot()
wenzelm@38640
   342
        val saved_color = gfx.getColor  // FIXME needed!?
wenzelm@38640
   343
        try {
wenzelm@38640
   344
          for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
wenzelm@38640
   345
            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38640
   346
            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
wenzelm@38640
   347
            val y = line_to_y(line1)
wenzelm@38640
   348
            val height = HEIGHT * (line2 - line1)
wenzelm@39044
   349
            gfx.setColor(Document_View.status_color(snapshot, command))
wenzelm@38640
   350
            gfx.fillRect(0, y, getWidth - 1, height)
wenzelm@38640
   351
          }
wenzelm@37188
   352
        }
wenzelm@38640
   353
        finally { gfx.setColor(saved_color) }
wenzelm@34784
   354
      }
wenzelm@34784
   355
    }
wenzelm@34784
   356
wenzelm@34784
   357
    private def line_to_y(line: Int): Int =
wenzelm@34784
   358
      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
wenzelm@34784
   359
wenzelm@34784
   360
    private def y_to_line(y: Int): Int =
wenzelm@34784
   361
      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
wenzelm@34784
   362
  }
immler@34403
   363
wenzelm@34784
   364
wenzelm@34784
   365
  /* activation */
wenzelm@34784
   366
wenzelm@34808
   367
  private def activate()
wenzelm@34784
   368
  {
wenzelm@34784
   369
    text_area.getPainter.
wenzelm@34784
   370
      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
wenzelm@39131
   371
    text_area.addFocusListener(focus_listener)
wenzelm@39131
   372
    text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
wenzelm@34810
   373
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   374
    text_area.addLeftOfScrollBar(overview)
wenzelm@37129
   375
    session.commands_changed += commands_changed_actor
wenzelm@34784
   376
  }
wenzelm@34784
   377
wenzelm@34808
   378
  private def deactivate()
wenzelm@34784
   379
  {
wenzelm@37129
   380
    session.commands_changed -= commands_changed_actor
wenzelm@39131
   381
    text_area.removeFocusListener(focus_listener)
wenzelm@39131
   382
    text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
wenzelm@39131
   383
    text_area.removeCaretListener(caret_listener)
wenzelm@34810
   384
    text_area.removeLeftOfScrollBar(overview)
wenzelm@34784
   385
    text_area.getPainter.removeExtension(text_area_extension)
wenzelm@34784
   386
  }
immler@34403
   387
}