src/Tools/jEdit/src/jedit/document_view.scala
author wenzelm
Sun Aug 29 15:09:11 2010 +0200 (2010-08-29)
changeset 38845 a9e37daf5bd0
parent 38843 d95522496593
child 38855 35b2d91e88d7
permissions -rw-r--r--
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
Markup_Tree.select: plain Iterator;
misc tuning and simplification;
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@38843
   106
          val buffer = model.buffer
wenzelm@38843
   107
          Isabelle.swing_buffer_lock(buffer) {
wenzelm@38151
   108
            val snapshot = model.snapshot()
wenzelm@38843
   109
            if (changed.exists(snapshot.node.commands.contains)) {
wenzelm@38843
   110
              var visible_change = false
wenzelm@38843
   111
              for ((command, start) <- snapshot.node.command_starts) {
wenzelm@38843
   112
                if (changed(command)) {
wenzelm@38843
   113
                  val stop = start + command.length
wenzelm@38843
   114
                  val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38843
   115
                  val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
wenzelm@38843
   116
                  if (line2 >= text_area.getFirstLine &&
wenzelm@38843
   117
                      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
wenzelm@38843
   118
                    visible_change = true
wenzelm@38843
   119
                  text_area.invalidateLineRange(line1, line2)
wenzelm@38843
   120
                }
wenzelm@38843
   121
              }
wenzelm@38843
   122
              // FIXME danger of deadlock!?
wenzelm@38843
   123
              if (visible_change) model.buffer.propertiesChanged()
wenzelm@38640
   124
wenzelm@38843
   125
              overview.repaint()  // FIXME really paint here!?
wenzelm@38640
   126
            }
wenzelm@34834
   127
          }
wenzelm@34784
   128
wenzelm@34784
   129
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@34784
   130
      }
immler@34403
   131
    }
immler@34678
   132
  }
immler@34403
   133
immler@34403
   134
wenzelm@34784
   135
  /* text_area_extension */
wenzelm@34784
   136
wenzelm@34784
   137
  private val text_area_extension = new TextAreaExtension
immler@34678
   138
  {
wenzelm@37685
   139
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@37685
   140
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@37685
   141
      start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
wenzelm@34784
   142
    {
wenzelm@38843
   143
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38843
   144
        val snapshot = model.snapshot()
wenzelm@38223
   145
wenzelm@38843
   146
        val command_range: Iterable[(Command, Text.Offset)] =
wenzelm@38843
   147
        {
wenzelm@38843
   148
          val range = snapshot.node.command_range(snapshot.revert(start(0)))
wenzelm@38843
   149
          if (range.hasNext) {
wenzelm@38843
   150
            val (cmd0, start0) = range.next
wenzelm@38843
   151
            new Iterable[(Command, Text.Offset)] {
wenzelm@38843
   152
              def iterator =
wenzelm@38843
   153
                Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
wenzelm@38843
   154
            }
wenzelm@38843
   155
          }
wenzelm@38843
   156
          else Iterable.empty
wenzelm@38843
   157
        }
wenzelm@38223
   158
wenzelm@38843
   159
        val saved_color = gfx.getColor
wenzelm@38843
   160
        try {
wenzelm@38843
   161
          var y = y0
wenzelm@38843
   162
          for (i <- 0 until physical_lines.length) {
wenzelm@38843
   163
            if (physical_lines(i) != -1) {
wenzelm@38843
   164
              val line_start = start(i)
wenzelm@38843
   165
              val line_end = model.visible_line_end(line_start, end(i))
wenzelm@38843
   166
wenzelm@38843
   167
              val a = snapshot.revert(line_start)
wenzelm@38843
   168
              val b = snapshot.revert(line_end)
wenzelm@38843
   169
              val cmds = command_range.iterator.
wenzelm@38843
   170
                dropWhile { case (cmd, c) => c + cmd.length <= a } .
wenzelm@38843
   171
                takeWhile { case (_, c) => c < b }
wenzelm@38843
   172
wenzelm@38843
   173
              for ((command, command_start) <- cmds if !command.is_ignored) {
wenzelm@38843
   174
                val p =
wenzelm@38843
   175
                  text_area.offsetToXY(line_start max snapshot.convert(command_start))
wenzelm@38843
   176
                val q =
wenzelm@38843
   177
                  text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
wenzelm@38843
   178
                assert(p.y == q.y)
wenzelm@38843
   179
                gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@38843
   180
                gfx.fillRect(p.x, y, q.x - p.x, line_height)
wenzelm@38843
   181
              }
wenzelm@38843
   182
            }
wenzelm@38843
   183
            y += line_height
wenzelm@38223
   184
          }
wenzelm@38223
   185
        }
wenzelm@38843
   186
        finally { gfx.setColor(saved_color) }
wenzelm@38223
   187
      }
wenzelm@34784
   188
    }
wenzelm@34784
   189
wenzelm@34784
   190
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   191
    {
wenzelm@38845
   192
      Isabelle.swing_buffer_lock(model.buffer) {
wenzelm@38845
   193
        val snapshot = model.snapshot()
wenzelm@38845
   194
        val offset = text_area.xyToOffset(x, y)
wenzelm@38845
   195
        val markup =
wenzelm@38845
   196
          snapshot.select_markup(Text.Range(offset, offset + 1)) {
wenzelm@38580
   197
            case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@38845
   198
              Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
wenzelm@38845
   199
          } { null }
wenzelm@38845
   200
        if (markup.hasNext) markup.next.info else null
wenzelm@34784
   201
      }
wenzelm@34734
   202
    }
immler@34678
   203
  }
immler@34513
   204
wenzelm@34784
   205
wenzelm@37129
   206
  /* caret handling */
wenzelm@34810
   207
wenzelm@37849
   208
  def selected_command(): Option[Command] =
wenzelm@38223
   209
  {
wenzelm@38223
   210
    Swing_Thread.require()
wenzelm@38151
   211
    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
wenzelm@38223
   212
  }
wenzelm@34810
   213
wenzelm@37849
   214
  private val caret_listener = new CaretListener {
wenzelm@37849
   215
    private val delay = Swing_Thread.delay_last(session.input_delay) {
wenzelm@37849
   216
      session.perspective.event(Session.Perspective)
wenzelm@34810
   217
    }
wenzelm@37849
   218
    override def caretUpdate(e: CaretEvent) { delay() }
wenzelm@34810
   219
  }
wenzelm@34810
   220
wenzelm@34810
   221
wenzelm@34784
   222
  /* overview of command status left of scrollbar */
wenzelm@34784
   223
wenzelm@34834
   224
  private val overview = new JPanel(new BorderLayout)
wenzelm@34784
   225
  {
wenzelm@34784
   226
    private val WIDTH = 10
wenzelm@34784
   227
    private val HEIGHT = 2
wenzelm@34784
   228
wenzelm@34806
   229
    setPreferredSize(new Dimension(WIDTH, 0))
wenzelm@34806
   230
wenzelm@34784
   231
    setRequestFocusEnabled(false)
wenzelm@34784
   232
wenzelm@34784
   233
    addMouseListener(new MouseAdapter {
wenzelm@34784
   234
      override def mousePressed(event: MouseEvent) {
wenzelm@34784
   235
        val line = y_to_line(event.getY)
wenzelm@34784
   236
        if (line >= 0 && line < text_area.getLineCount)
wenzelm@34784
   237
          text_area.setCaretPosition(text_area.getLineStartOffset(line))
wenzelm@34784
   238
      }
wenzelm@34784
   239
    })
wenzelm@34784
   240
wenzelm@34784
   241
    override def addNotify() {
wenzelm@34784
   242
      super.addNotify()
wenzelm@34784
   243
      ToolTipManager.sharedInstance.registerComponent(this)
wenzelm@34784
   244
    }
immler@34403
   245
wenzelm@34784
   246
    override def removeNotify() {
wenzelm@34784
   247
      ToolTipManager.sharedInstance.unregisterComponent(this)
wenzelm@34784
   248
      super.removeNotify
wenzelm@34784
   249
    }
wenzelm@34784
   250
wenzelm@34784
   251
    override def getToolTipText(event: MouseEvent): String =
wenzelm@34784
   252
    {
wenzelm@34784
   253
      val line = y_to_line(event.getY())
wenzelm@34784
   254
      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
wenzelm@34784
   255
      else ""
wenzelm@34784
   256
    }
wenzelm@34784
   257
wenzelm@34784
   258
    override def paintComponent(gfx: Graphics)
wenzelm@34784
   259
    {
wenzelm@34784
   260
      super.paintComponent(gfx)
wenzelm@38640
   261
      Swing_Thread.assert()
wenzelm@34784
   262
      val buffer = model.buffer
wenzelm@38843
   263
      Isabelle.buffer_lock(buffer) {
wenzelm@38640
   264
        val snapshot = model.snapshot()
wenzelm@38640
   265
        val saved_color = gfx.getColor  // FIXME needed!?
wenzelm@38640
   266
        try {
wenzelm@38640
   267
          for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
wenzelm@38640
   268
            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
wenzelm@38640
   269
            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
wenzelm@38640
   270
            val y = line_to_y(line1)
wenzelm@38640
   271
            val height = HEIGHT * (line2 - line1)
wenzelm@38640
   272
            gfx.setColor(Document_View.choose_color(snapshot, command))
wenzelm@38640
   273
            gfx.fillRect(0, y, getWidth - 1, height)
wenzelm@38640
   274
          }
wenzelm@37188
   275
        }
wenzelm@38640
   276
        finally { gfx.setColor(saved_color) }
wenzelm@34784
   277
      }
wenzelm@34784
   278
    }
wenzelm@34784
   279
wenzelm@34784
   280
    private def line_to_y(line: Int): Int =
wenzelm@34784
   281
      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
wenzelm@34784
   282
wenzelm@34784
   283
    private def y_to_line(y: Int): Int =
wenzelm@34784
   284
      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
wenzelm@34784
   285
  }
immler@34403
   286
wenzelm@34784
   287
wenzelm@34784
   288
  /* activation */
wenzelm@34784
   289
wenzelm@34808
   290
  private def activate()
wenzelm@34784
   291
  {
wenzelm@34784
   292
    text_area.getPainter.
wenzelm@34784
   293
      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
wenzelm@34810
   294
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   295
    text_area.addLeftOfScrollBar(overview)
wenzelm@37129
   296
    session.commands_changed += commands_changed_actor
wenzelm@34784
   297
  }
wenzelm@34784
   298
wenzelm@34808
   299
  private def deactivate()
wenzelm@34784
   300
  {
wenzelm@37129
   301
    session.commands_changed -= commands_changed_actor
wenzelm@34810
   302
    text_area.removeLeftOfScrollBar(overview)
wenzelm@34810
   303
    text_area.removeCaretListener(caret_listener)
wenzelm@34784
   304
    text_area.getPainter.removeExtension(text_area_extension)
wenzelm@34784
   305
  }
immler@34403
   306
}