src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Sat Sep 04 22:36:42 2010 +0200 (2010-09-04)
changeset 39132 ba17ca3acdd3
parent 39131 947c62440026
child 39168 e3ac771235f7
permissions -rw-r--r--
refined treatment of multi-line subexpressions;
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@39132
   127
  def invalidate_line_range(range: Text.Range)
wenzelm@39132
   128
  {
wenzelm@39132
   129
    text_area.invalidateLineRange(
wenzelm@39132
   130
      model.buffer.getLineOfOffset(range.start),
wenzelm@39132
   131
      model.buffer.getLineOfOffset(range.stop))
wenzelm@39132
   132
  }
wenzelm@39132
   133
wenzelm@38881
   134
wenzelm@37129
   135
  /* commands_changed_actor */
wenzelm@34834
   136
wenzelm@37129
   137
  private val commands_changed_actor = actor {
wenzelm@34784
   138
    loop {
wenzelm@34784
   139
      react {
wenzelm@38360
   140
        case Session.Commands_Changed(changed) =>
wenzelm@38843
   141
          val buffer = model.buffer
wenzelm@38843
   142
          Isabelle.swing_buffer_lock(buffer) {
wenzelm@38151
   143
            val snapshot = model.snapshot()
wenzelm@38881
   144
wenzelm@38884
   145
            if (changed.exists(snapshot.node.commands.contains))
wenzelm@38884
   146
              overview.repaint()
wenzelm@38884
   147
wenzelm@38881
   148
            val visible_range = screen_lines_range()
wenzelm@38881
   149
            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
wenzelm@38881
   150
            if (visible_cmds.exists(changed)) {
wenzelm@38881
   151
              for {
wenzelm@38881
   152
                line <- 0 until text_area.getVisibleLines
wenzelm@38881
   153
                val start = text_area.getScreenLineStartOffset(line) if start >= 0
wenzelm@38881
   154
                val end = text_area.getScreenLineEndOffset(line) if end >= 0
wenzelm@38881
   155
                val range = proper_line_range(start, end)
wenzelm@38881
   156
                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
wenzelm@38881
   157
                if line_cmds.exists(changed)
wenzelm@38881
   158
              } text_area.invalidateScreenLineRange(line, line)
wenzelm@38884
   159
wenzelm@38843
   160
              // FIXME danger of deadlock!?
wenzelm@38881
   161
              // FIXME potentially slow!?
wenzelm@38881
   162
              model.buffer.propertiesChanged()
wenzelm@38640
   163
            }
wenzelm@34834
   164
          }
wenzelm@34784
   165
wenzelm@34784
   166
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@34784
   167
      }
immler@34403
   168
    }
immler@34678
   169
  }
immler@34403
   170
immler@34403
   171
wenzelm@39131
   172
  /* subexpression highlighting */
wenzelm@39131
   173
wenzelm@39132
   174
  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
wenzelm@39132
   175
  {
wenzelm@39132
   176
    val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
wenzelm@39132
   177
    {
wenzelm@39132
   178
      case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) =>
wenzelm@39132
   179
        Some(snapshot.convert(range))
wenzelm@39132
   180
    }
wenzelm@39132
   181
    val offset = text_area.xyToOffset(x, y)
wenzelm@39132
   182
    val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
wenzelm@39132
   183
    if (markup.hasNext) markup.next.info else None
wenzelm@39132
   184
  }
wenzelm@39132
   185
wenzelm@39132
   186
  private var highlight_range: Option[Text.Range] = None
wenzelm@39131
   187
wenzelm@39131
   188
  private val focus_listener = new FocusAdapter {
wenzelm@39132
   189
    override def focusLost(e: FocusEvent) { highlight_range = None }
wenzelm@39131
   190
  }
wenzelm@39131
   191
wenzelm@39131
   192
  private val mouse_motion_listener = new MouseMotionAdapter {
wenzelm@39131
   193
    override def mouseMoved(e: MouseEvent) {
wenzelm@39131
   194
      val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
wenzelm@39132
   195
      if (!model.buffer.isLoaded) highlight_range = None
wenzelm@39132
   196
      else
wenzelm@39132
   197
        Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@39132
   198
          highlight_range.map(invalidate_line_range(_))
wenzelm@39132
   199
          highlight_range =
wenzelm@39132
   200
            if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
wenzelm@39132
   201
          highlight_range.map(invalidate_line_range(_))
wenzelm@39132
   202
        }
wenzelm@39131
   203
    }
wenzelm@39131
   204
  }
wenzelm@39131
   205
wenzelm@39131
   206
wenzelm@34784
   207
  /* text_area_extension */
wenzelm@34784
   208
wenzelm@34784
   209
  private val text_area_extension = new TextAreaExtension
immler@34678
   210
  {
wenzelm@37685
   211
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@37685
   212
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@38886
   213
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@34784
   214
    {
wenzelm@38843
   215
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38843
   216
        val snapshot = model.snapshot()
wenzelm@38843
   217
        val saved_color = gfx.getColor
wenzelm@39044
   218
        val ascent = text_area.getPainter.getFontMetrics.getAscent
wenzelm@39131
   219
wenzelm@38843
   220
        try {
wenzelm@38843
   221
          for (i <- 0 until physical_lines.length) {
wenzelm@38843
   222
            if (physical_lines(i) != -1) {
wenzelm@38881
   223
              val line_range = proper_line_range(start(i), end(i))
wenzelm@39044
   224
wenzelm@39044
   225
              // background color
wenzelm@38880
   226
              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
wenzelm@39044
   227
              for {
wenzelm@39044
   228
                (command, command_start) <- cmds if !command.is_ignored
wenzelm@38880
   229
                val range = line_range.restrict(snapshot.convert(command.range + command_start))
wenzelm@39044
   230
                r <- Isabelle.gfx_range(text_area, range)
wenzelm@39044
   231
              } {
wenzelm@39044
   232
                gfx.setColor(Document_View.status_color(snapshot, command))
wenzelm@39044
   233
                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
wenzelm@39044
   234
              }
wenzelm@39044
   235
wenzelm@39132
   236
              // subexpression highlighting -- potentially from other snapshot
wenzelm@39132
   237
              if (highlight_range.isDefined) {
wenzelm@39132
   238
                if (line_range.overlaps(highlight_range.get)) {
wenzelm@39132
   239
                  Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
wenzelm@39131
   240
                    case None =>
wenzelm@39131
   241
                    case Some(r) =>
wenzelm@39131
   242
                      gfx.setColor(Color.black)
wenzelm@39131
   243
                      gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
wenzelm@39131
   244
                  }
wenzelm@39131
   245
                }
wenzelm@39131
   246
              }
wenzelm@39131
   247
wenzelm@39044
   248
              // squiggly underline
wenzelm@39044
   249
              for {
wenzelm@39044
   250
                Text.Info(range, color) <-
wenzelm@39044
   251
                  snapshot.select_markup(line_range)(Document_View.message_markup)(null)
wenzelm@39044
   252
                if color != null
wenzelm@39044
   253
                r <- Isabelle.gfx_range(text_area, range)
wenzelm@39044
   254
              } {
wenzelm@39044
   255
                gfx.setColor(color)
wenzelm@39044
   256
                val x0 = (r.x / 2) * 2
wenzelm@39044
   257
                val y0 = r.y + ascent + 1
wenzelm@39044
   258
                for (x1 <- Range(x0, x0 + r.length, 2)) {
wenzelm@39044
   259
                  val y1 = if (x1 % 4 < 2) y0 else y0 + 1
wenzelm@39044
   260
                  gfx.drawLine(x1, y1, x1 + 1, y1)
wenzelm@38883
   261
                }
wenzelm@38843
   262
              }
wenzelm@38843
   263
            }
wenzelm@38223
   264
          }
wenzelm@38223
   265
        }
wenzelm@38843
   266
        finally { gfx.setColor(saved_color) }
wenzelm@38223
   267
      }
wenzelm@34784
   268
    }
wenzelm@34784
   269
wenzelm@34784
   270
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   271
    {
wenzelm@38845
   272
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38845
   273
        val snapshot = model.snapshot()
wenzelm@38845
   274
        val offset = text_area.xyToOffset(x, y)
wenzelm@38845
   275
        val markup =
wenzelm@38845
   276
          snapshot.select_markup(Text.Range(offset, offset + 1)) {
wenzelm@38580
   277
            case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@38845
   278
              Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
wenzelm@38845
   279
          } { null }
wenzelm@38845
   280
        if (markup.hasNext) markup.next.info else null
wenzelm@34784
   281
      }
wenzelm@34734
   282
    }
immler@34678
   283
  }
immler@34513
   284
wenzelm@34784
   285
wenzelm@37129
   286
  /* caret handling */
wenzelm@34810
   287
wenzelm@37849
   288
  def selected_command(): Option[Command] =
wenzelm@38223
   289
  {
wenzelm@38223
   290
    Swing_Thread.require()
wenzelm@38151
   291
    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
wenzelm@38223
   292
  }
wenzelm@34810
   293
wenzelm@37849
   294
  private val caret_listener = new CaretListener {
wenzelm@37849
   295
    private val delay = Swing_Thread.delay_last(session.input_delay) {
wenzelm@37849
   296
      session.perspective.event(Session.Perspective)
wenzelm@34810
   297
    }
wenzelm@37849
   298
    override def caretUpdate(e: CaretEvent) { delay() }
wenzelm@34810
   299
  }
wenzelm@34810
   300
wenzelm@34810
   301
wenzelm@34784
   302
  /* overview of command status left of scrollbar */
wenzelm@34784
   303
wenzelm@34834
   304
  private val overview = new JPanel(new BorderLayout)
wenzelm@34784
   305
  {
wenzelm@34784
   306
    private val WIDTH = 10
wenzelm@34784
   307
    private val HEIGHT = 2
wenzelm@34784
   308
wenzelm@34806
   309
    setPreferredSize(new Dimension(WIDTH, 0))
wenzelm@34806
   310
wenzelm@34784
   311
    setRequestFocusEnabled(false)
wenzelm@34784
   312
wenzelm@34784
   313
    addMouseListener(new MouseAdapter {
wenzelm@34784
   314
      override def mousePressed(event: MouseEvent) {
wenzelm@34784
   315
        val line = y_to_line(event.getY)
wenzelm@34784
   316
        if (line >= 0 && line < text_area.getLineCount)
wenzelm@34784
   317
          text_area.setCaretPosition(text_area.getLineStartOffset(line))
wenzelm@34784
   318
      }
wenzelm@34784
   319
    })
wenzelm@34784
   320
wenzelm@34784
   321
    override def addNotify() {
wenzelm@34784
   322
      super.addNotify()
wenzelm@34784
   323
      ToolTipManager.sharedInstance.registerComponent(this)
wenzelm@34784
   324
    }
immler@34403
   325
wenzelm@34784
   326
    override def removeNotify() {
wenzelm@34784
   327
      ToolTipManager.sharedInstance.unregisterComponent(this)
wenzelm@34784
   328
      super.removeNotify
wenzelm@34784
   329
    }
wenzelm@34784
   330
wenzelm@34784
   331
    override def getToolTipText(event: MouseEvent): String =
wenzelm@34784
   332
    {
wenzelm@34784
   333
      val line = y_to_line(event.getY())
wenzelm@34784
   334
      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
wenzelm@34784
   335
      else ""
wenzelm@34784
   336
    }
wenzelm@34784
   337
wenzelm@34784
   338
    override def paintComponent(gfx: Graphics)
wenzelm@34784
   339
    {
wenzelm@34784
   340
      super.paintComponent(gfx)
wenzelm@38640
   341
      Swing_Thread.assert()
wenzelm@34784
   342
      val buffer = model.buffer
wenzelm@38843
   343
      Isabelle.buffer_lock(buffer) {
wenzelm@38640
   344
        val snapshot = model.snapshot()
wenzelm@38640
   345
        val saved_color = gfx.getColor  // FIXME needed!?
wenzelm@38640
   346
        try {
wenzelm@38640
   347
          for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
wenzelm@38640
   348
            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38640
   349
            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
wenzelm@38640
   350
            val y = line_to_y(line1)
wenzelm@38640
   351
            val height = HEIGHT * (line2 - line1)
wenzelm@39044
   352
            gfx.setColor(Document_View.status_color(snapshot, command))
wenzelm@38640
   353
            gfx.fillRect(0, y, getWidth - 1, height)
wenzelm@38640
   354
          }
wenzelm@37188
   355
        }
wenzelm@38640
   356
        finally { gfx.setColor(saved_color) }
wenzelm@34784
   357
      }
wenzelm@34784
   358
    }
wenzelm@34784
   359
wenzelm@34784
   360
    private def line_to_y(line: Int): Int =
wenzelm@34784
   361
      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
wenzelm@34784
   362
wenzelm@34784
   363
    private def y_to_line(y: Int): Int =
wenzelm@34784
   364
      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
wenzelm@34784
   365
  }
immler@34403
   366
wenzelm@34784
   367
wenzelm@34784
   368
  /* activation */
wenzelm@34784
   369
wenzelm@34808
   370
  private def activate()
wenzelm@34784
   371
  {
wenzelm@34784
   372
    text_area.getPainter.
wenzelm@34784
   373
      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
wenzelm@39131
   374
    text_area.addFocusListener(focus_listener)
wenzelm@39131
   375
    text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
wenzelm@34810
   376
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   377
    text_area.addLeftOfScrollBar(overview)
wenzelm@37129
   378
    session.commands_changed += commands_changed_actor
wenzelm@34784
   379
  }
wenzelm@34784
   380
wenzelm@34808
   381
  private def deactivate()
wenzelm@34784
   382
  {
wenzelm@37129
   383
    session.commands_changed -= commands_changed_actor
wenzelm@39131
   384
    text_area.removeFocusListener(focus_listener)
wenzelm@39131
   385
    text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
wenzelm@39131
   386
    text_area.removeCaretListener(caret_listener)
wenzelm@34810
   387
    text_area.removeLeftOfScrollBar(overview)
wenzelm@34784
   388
    text_area.getPainter.removeExtension(text_area_extension)
wenzelm@34784
   389
  }
immler@34403
   390
}