src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Mon Aug 23 17:35:47 2010 +0200 (2010-08-23)
changeset 38640 105d1f112da5
parent 38582 3a6ce43d99b1
child 38660 049fdf15144f
permissions -rw-r--r--
sporadic locking of jEdit buffer;
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@34784
    15
import java.awt.event.{MouseAdapter, MouseEvent}
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@34709
    20
import org.gjt.sp.jedit.gui.RolloverButton
wenzelm@34784
    21
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
wenzelm@37241
    22
import org.gjt.sp.jedit.syntax.SyntaxStyle
wenzelm@34784
    23
wenzelm@34784
    24
wenzelm@34784
    25
object Document_View
wenzelm@34784
    26
{
wenzelm@38227
    27
  def choose_color(snapshot: Document.Snapshot, command: Command): Color =
wenzelm@34784
    28
  {
wenzelm@38356
    29
    val state = snapshot.state(command)
wenzelm@38151
    30
    if (snapshot.is_outdated) new Color(240, 240, 240)
wenzelm@37186
    31
    else
wenzelm@38567
    32
      Isar_Document.command_status(state.status) match {
wenzelm@38567
    33
        case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
wenzelm@38567
    34
        case Isar_Document.Finished => new Color(234, 248, 255)
wenzelm@38567
    35
        case Isar_Document.Failed => new Color(255, 193, 193)
wenzelm@38567
    36
        case Isar_Document.Unprocessed => new Color(255, 228, 225)
wenzelm@38429
    37
        case _ => Color.red
wenzelm@37186
    38
      }
wenzelm@34784
    39
  }
wenzelm@34784
    40
wenzelm@34784
    41
wenzelm@34784
    42
  /* document view of text area */
wenzelm@34784
    43
wenzelm@34784
    44
  private val key = new Object
wenzelm@34784
    45
wenzelm@34784
    46
  def init(model: Document_Model, text_area: TextArea): Document_View =
wenzelm@34784
    47
  {
wenzelm@38223
    48
    Swing_Thread.require()
wenzelm@34784
    49
    val doc_view = new Document_View(model, text_area)
wenzelm@34784
    50
    text_area.putClientProperty(key, doc_view)
wenzelm@34784
    51
    doc_view.activate()
wenzelm@34784
    52
    doc_view
wenzelm@34784
    53
  }
wenzelm@34784
    54
wenzelm@34788
    55
  def apply(text_area: TextArea): Option[Document_View] =
wenzelm@34784
    56
  {
wenzelm@38223
    57
    Swing_Thread.require()
wenzelm@34784
    58
    text_area.getClientProperty(key) match {
wenzelm@34784
    59
      case doc_view: Document_View => Some(doc_view)
wenzelm@34784
    60
      case _ => None
wenzelm@34784
    61
    }
wenzelm@34784
    62
  }
wenzelm@34784
    63
wenzelm@34784
    64
  def exit(text_area: TextArea)
wenzelm@34784
    65
  {
wenzelm@38223
    66
    Swing_Thread.require()
wenzelm@34788
    67
    apply(text_area) match {
wenzelm@34784
    68
      case None => error("No document view for text area: " + text_area)
wenzelm@34784
    69
      case Some(doc_view) =>
wenzelm@34784
    70
        doc_view.deactivate()
wenzelm@34784
    71
        text_area.putClientProperty(key, null)
wenzelm@34784
    72
    }
wenzelm@34784
    73
  }
wenzelm@34784
    74
}
immler@34403
    75
wenzelm@34733
    76
wenzelm@37129
    77
class Document_View(val model: Document_Model, text_area: TextArea)
immler@34654
    78
{
wenzelm@34784
    79
  private val session = model.session
wenzelm@34784
    80
immler@34403
    81
wenzelm@37241
    82
  /* extended token styles */
wenzelm@37241
    83
wenzelm@37241
    84
  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
wenzelm@37241
    85
wenzelm@37241
    86
  def extend_styles()
wenzelm@37241
    87
  {
wenzelm@38223
    88
    Swing_Thread.require()
wenzelm@38158
    89
    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
wenzelm@37241
    90
  }
wenzelm@37241
    91
  extend_styles()
wenzelm@37241
    92
wenzelm@37241
    93
  def set_styles()
wenzelm@37241
    94
  {
wenzelm@38223
    95
    Swing_Thread.require()
wenzelm@37241
    96
    text_area.getPainter.setStyles(styles)
wenzelm@37241
    97
  }
wenzelm@37241
    98
wenzelm@37241
    99
wenzelm@37129
   100
  /* commands_changed_actor */
wenzelm@34834
   101
wenzelm@37129
   102
  private val commands_changed_actor = actor {
wenzelm@34784
   103
    loop {
wenzelm@34784
   104
      react {
wenzelm@38360
   105
        case Session.Commands_Changed(changed) =>
wenzelm@34834
   106
          Swing_Thread.now {
wenzelm@37685
   107
            // FIXME cover doc states as well!!?
wenzelm@38151
   108
            val snapshot = model.snapshot()
wenzelm@38640
   109
            val buffer = model.buffer
wenzelm@38640
   110
            Isabelle.buffer_read_lock(buffer) {
wenzelm@38640
   111
              if (changed.exists(snapshot.node.commands.contains)) {
wenzelm@38640
   112
                var visible_change = false
wenzelm@38640
   113
wenzelm@38640
   114
                for ((command, start) <- snapshot.node.command_starts) {
wenzelm@38640
   115
                  if (changed(command)) {
wenzelm@38640
   116
                    val stop = start + command.length
wenzelm@38640
   117
                    val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38640
   118
                    val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
wenzelm@38640
   119
                    if (line2 >= text_area.getFirstLine &&
wenzelm@38640
   120
                        line1 <= text_area.getFirstLine + text_area.getVisibleLines)
wenzelm@38640
   121
                      visible_change = true
wenzelm@38640
   122
                    text_area.invalidateLineRange(line1, line2)
wenzelm@38640
   123
                  }
wenzelm@38640
   124
                }
wenzelm@38640
   125
                if (visible_change) model.buffer.propertiesChanged()
wenzelm@38640
   126
wenzelm@38640
   127
                overview.repaint()  // FIXME paint here!?
wenzelm@38640
   128
              }
wenzelm@38640
   129
            }
wenzelm@34834
   130
          }
wenzelm@34784
   131
wenzelm@34784
   132
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@34784
   133
      }
immler@34403
   134
    }
immler@34678
   135
  }
immler@34403
   136
immler@34403
   137
wenzelm@34784
   138
  /* text_area_extension */
wenzelm@34784
   139
wenzelm@34784
   140
  private val text_area_extension = new TextAreaExtension
immler@34678
   141
  {
wenzelm@37685
   142
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@37685
   143
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@37685
   144
      start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
wenzelm@34784
   145
    {
wenzelm@38223
   146
      Swing_Thread.assert()
wenzelm@38223
   147
wenzelm@38223
   148
      val snapshot = model.snapshot()
wenzelm@38223
   149
wenzelm@38426
   150
      val command_range: Iterable[(Command, Text.Offset)] =
wenzelm@38223
   151
      {
wenzelm@38223
   152
        val range = snapshot.node.command_range(snapshot.revert(start(0)))
wenzelm@38223
   153
        if (range.hasNext) {
wenzelm@38223
   154
          val (cmd0, start0) = range.next
wenzelm@38426
   155
          new Iterable[(Command, Text.Offset)] {
wenzelm@38227
   156
            def iterator =
wenzelm@38227
   157
              Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
wenzelm@38223
   158
          }
wenzelm@38223
   159
        }
wenzelm@38223
   160
        else Iterable.empty
wenzelm@38223
   161
      }
wenzelm@37555
   162
wenzelm@38223
   163
      val saved_color = gfx.getColor
wenzelm@38223
   164
      try {
wenzelm@38223
   165
        var y = y0
wenzelm@38223
   166
        for (i <- 0 until physical_lines.length) {
wenzelm@38223
   167
          if (physical_lines(i) != -1) {
wenzelm@38223
   168
            val line_start = start(i)
wenzelm@38223
   169
            val line_end = model.visible_line_end(line_start, end(i))
wenzelm@38223
   170
wenzelm@38223
   171
            val a = snapshot.revert(line_start)
wenzelm@38223
   172
            val b = snapshot.revert(line_end)
wenzelm@38223
   173
            val cmds = command_range.iterator.
wenzelm@38223
   174
              dropWhile { case (cmd, c) => c + cmd.length <= a } .
wenzelm@38223
   175
              takeWhile { case (_, c) => c < b }
wenzelm@38223
   176
wenzelm@38223
   177
            for ((command, command_start) <- cmds if !command.is_ignored) {
wenzelm@38223
   178
              val p =
wenzelm@38223
   179
                text_area.offsetToXY(line_start max snapshot.convert(command_start))
wenzelm@38223
   180
              val q =
wenzelm@38223
   181
                text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
wenzelm@38223
   182
              assert(p.y == q.y)
wenzelm@38223
   183
              gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@38223
   184
              gfx.fillRect(p.x, y, q.x - p.x, line_height)
wenzelm@37685
   185
            }
wenzelm@37685
   186
          }
wenzelm@38223
   187
          y += line_height
wenzelm@37685
   188
        }
wenzelm@34784
   189
      }
wenzelm@38223
   190
      finally { gfx.setColor(saved_color) }
wenzelm@34784
   191
    }
wenzelm@34784
   192
wenzelm@34784
   193
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   194
    {
wenzelm@38223
   195
      Swing_Thread.assert()
wenzelm@38223
   196
wenzelm@38151
   197
      val snapshot = model.snapshot()
wenzelm@38153
   198
      val offset = snapshot.revert(text_area.xyToOffset(x, y))
wenzelm@38152
   199
      snapshot.node.command_at(offset) match {
wenzelm@34855
   200
        case Some((command, command_start)) =>
wenzelm@38582
   201
          (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
wenzelm@38580
   202
            case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@38574
   203
              val typing =
wenzelm@38574
   204
                Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
wenzelm@38574
   205
              Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))
wenzelm@38582
   206
          } { null }).head.info
wenzelm@34784
   207
        case None => null
wenzelm@34784
   208
      }
wenzelm@34734
   209
    }
immler@34678
   210
  }
immler@34513
   211
wenzelm@34784
   212
wenzelm@37129
   213
  /* caret handling */
wenzelm@34810
   214
wenzelm@37849
   215
  def selected_command(): Option[Command] =
wenzelm@38223
   216
  {
wenzelm@38223
   217
    Swing_Thread.require()
wenzelm@38151
   218
    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
wenzelm@38223
   219
  }
wenzelm@34810
   220
wenzelm@37849
   221
  private val caret_listener = new CaretListener {
wenzelm@37849
   222
    private val delay = Swing_Thread.delay_last(session.input_delay) {
wenzelm@37849
   223
      session.perspective.event(Session.Perspective)
wenzelm@34810
   224
    }
wenzelm@37849
   225
    override def caretUpdate(e: CaretEvent) { delay() }
wenzelm@34810
   226
  }
wenzelm@34810
   227
wenzelm@34810
   228
wenzelm@34784
   229
  /* overview of command status left of scrollbar */
wenzelm@34784
   230
wenzelm@34834
   231
  private val overview = new JPanel(new BorderLayout)
wenzelm@34784
   232
  {
wenzelm@34784
   233
    private val WIDTH = 10
wenzelm@34784
   234
    private val HEIGHT = 2
wenzelm@34784
   235
wenzelm@34806
   236
    setPreferredSize(new Dimension(WIDTH, 0))
wenzelm@34806
   237
wenzelm@34784
   238
    setRequestFocusEnabled(false)
wenzelm@34784
   239
wenzelm@34784
   240
    addMouseListener(new MouseAdapter {
wenzelm@34784
   241
      override def mousePressed(event: MouseEvent) {
wenzelm@34784
   242
        val line = y_to_line(event.getY)
wenzelm@34784
   243
        if (line >= 0 && line < text_area.getLineCount)
wenzelm@34784
   244
          text_area.setCaretPosition(text_area.getLineStartOffset(line))
wenzelm@34784
   245
      }
wenzelm@34784
   246
    })
wenzelm@34784
   247
wenzelm@34784
   248
    override def addNotify() {
wenzelm@34784
   249
      super.addNotify()
wenzelm@34784
   250
      ToolTipManager.sharedInstance.registerComponent(this)
wenzelm@34784
   251
    }
immler@34403
   252
wenzelm@34784
   253
    override def removeNotify() {
wenzelm@34784
   254
      ToolTipManager.sharedInstance.unregisterComponent(this)
wenzelm@34784
   255
      super.removeNotify
wenzelm@34784
   256
    }
wenzelm@34784
   257
wenzelm@34784
   258
    override def getToolTipText(event: MouseEvent): String =
wenzelm@34784
   259
    {
wenzelm@34784
   260
      val line = y_to_line(event.getY())
wenzelm@34784
   261
      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
wenzelm@34784
   262
      else ""
wenzelm@34784
   263
    }
wenzelm@34784
   264
wenzelm@34784
   265
    override def paintComponent(gfx: Graphics)
wenzelm@34784
   266
    {
wenzelm@34784
   267
      super.paintComponent(gfx)
wenzelm@38640
   268
      Swing_Thread.assert()
wenzelm@34784
   269
      val buffer = model.buffer
wenzelm@38640
   270
      Isabelle.buffer_read_lock(buffer) {
wenzelm@38640
   271
        val snapshot = model.snapshot()
wenzelm@38640
   272
        val saved_color = gfx.getColor  // FIXME needed!?
wenzelm@38640
   273
        try {
wenzelm@38640
   274
          for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
wenzelm@38640
   275
            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38640
   276
            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
wenzelm@38640
   277
            val y = line_to_y(line1)
wenzelm@38640
   278
            val height = HEIGHT * (line2 - line1)
wenzelm@38640
   279
            gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@38640
   280
            gfx.fillRect(0, y, getWidth - 1, height)
wenzelm@38640
   281
          }
wenzelm@37188
   282
        }
wenzelm@38640
   283
        finally { gfx.setColor(saved_color) }
wenzelm@34784
   284
      }
wenzelm@34784
   285
    }
wenzelm@34784
   286
wenzelm@34784
   287
    private def line_to_y(line: Int): Int =
wenzelm@34784
   288
      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
wenzelm@34784
   289
wenzelm@34784
   290
    private def y_to_line(y: Int): Int =
wenzelm@34784
   291
      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
wenzelm@34784
   292
  }
immler@34403
   293
wenzelm@34784
   294
wenzelm@34784
   295
  /* activation */
wenzelm@34784
   296
wenzelm@34808
   297
  private def activate()
wenzelm@34784
   298
  {
wenzelm@34784
   299
    text_area.getPainter.
wenzelm@34784
   300
      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
wenzelm@34810
   301
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   302
    text_area.addLeftOfScrollBar(overview)
wenzelm@37129
   303
    session.commands_changed += commands_changed_actor
wenzelm@34784
   304
  }
wenzelm@34784
   305
wenzelm@34808
   306
  private def deactivate()
wenzelm@34784
   307
  {
wenzelm@37129
   308
    session.commands_changed -= commands_changed_actor
wenzelm@34810
   309
    text_area.removeLeftOfScrollBar(overview)
wenzelm@34810
   310
    text_area.removeCaretListener(caret_listener)
wenzelm@34784
   311
    text_area.getPainter.removeExtension(text_area_extension)
wenzelm@34784
   312
  }
immler@34403
   313
}