src/Tools/jEdit/src/timing_dockable.scala
author wenzelm
Sat Aug 24 13:32:51 2013 +0200 (2013-08-24)
changeset 53177 dcac8d837b9c
parent 52980 28f59ca8ce78
child 53711 8ce7795256e1
permissions -rw-r--r--
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm@51533
     1
/*  Title:      Tools/jEdit/src/timing_dockable.scala
wenzelm@51533
     2
    Author:     Makarius
wenzelm@51533
     3
wenzelm@51533
     4
Dockable window for timing information.
wenzelm@51533
     5
*/
wenzelm@51533
     6
wenzelm@51533
     7
package isabelle.jedit
wenzelm@51533
     8
wenzelm@51533
     9
wenzelm@51533
    10
import isabelle._
wenzelm@51533
    11
wenzelm@51533
    12
import scala.actors.Actor._
wenzelm@51533
    13
import scala.swing.{FlowPanel, Label, ListView, Alignment, ScrollPane, Component, TextField}
wenzelm@51538
    14
import scala.swing.event.{MouseClicked, ValueChanged}
wenzelm@51533
    15
wenzelm@51533
    16
import java.lang.System
wenzelm@51536
    17
import java.awt.{BorderLayout, Graphics2D, Insets, Color}
wenzelm@51533
    18
import javax.swing.{JList, BorderFactory}
wenzelm@51533
    19
import javax.swing.border.{BevelBorder, SoftBevelBorder}
wenzelm@51533
    20
wenzelm@51533
    21
import org.gjt.sp.jedit.{View, jEdit}
wenzelm@51533
    22
wenzelm@51533
    23
wenzelm@51533
    24
class Timing_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@51533
    25
{
wenzelm@51533
    26
  /* entry */
wenzelm@51533
    27
wenzelm@51533
    28
  private object Entry
wenzelm@51533
    29
  {
wenzelm@51533
    30
    object Ordering extends scala.math.Ordering[Entry]
wenzelm@51533
    31
    {
wenzelm@51533
    32
      def compare(entry1: Entry, entry2: Entry): Int =
wenzelm@51533
    33
        entry2.timing compare entry1.timing
wenzelm@51533
    34
    }
wenzelm@51533
    35
wenzelm@51533
    36
    object Renderer_Component extends Label
wenzelm@51533
    37
    {
wenzelm@51533
    38
      opaque = false
wenzelm@51533
    39
      xAlignment = Alignment.Leading
wenzelm@51533
    40
      border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
wenzelm@51536
    41
wenzelm@51536
    42
      var entry: Entry = null
wenzelm@51536
    43
      override def paintComponent(gfx: Graphics2D)
wenzelm@51536
    44
      {
wenzelm@51536
    45
        def paint_rectangle(color: Color)
wenzelm@51536
    46
        {
wenzelm@51536
    47
          val size = peer.getSize()
wenzelm@51536
    48
          val insets = border.getBorderInsets(peer)
wenzelm@51536
    49
          val x = insets.left
wenzelm@51536
    50
          val y = insets.top
wenzelm@51536
    51
          val w = size.width - x - insets.right
wenzelm@51536
    52
          val h = size.height - y - insets.bottom
wenzelm@51536
    53
          gfx.setColor(color)
wenzelm@51536
    54
          gfx.fillRect(x, y, w, h)
wenzelm@51536
    55
        }
wenzelm@51536
    56
wenzelm@51536
    57
        entry match {
wenzelm@51536
    58
          case theory_entry: Theory_Entry if theory_entry.current =>
wenzelm@51536
    59
            paint_rectangle(view.getTextArea.getPainter.getSelectionColor)
wenzelm@51536
    60
          case _: Command_Entry =>
wenzelm@51536
    61
            paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor)
wenzelm@51536
    62
          case _ =>
wenzelm@51536
    63
        }
wenzelm@51536
    64
        super.paintComponent(gfx)
wenzelm@51536
    65
      }
wenzelm@51533
    66
    }
wenzelm@51533
    67
wenzelm@51533
    68
    class Renderer extends ListView.Renderer[Entry]
wenzelm@51533
    69
    {
wenzelm@51533
    70
      def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
wenzelm@51533
    71
        entry: Entry, index: Int): Component =
wenzelm@51533
    72
      {
wenzelm@51533
    73
        val component = Renderer_Component
wenzelm@51536
    74
        component.entry = entry
wenzelm@51534
    75
        component.text = entry.print
wenzelm@51533
    76
        component
wenzelm@51533
    77
      }
wenzelm@51533
    78
    }
wenzelm@51533
    79
  }
wenzelm@51533
    80
wenzelm@51534
    81
  private abstract class Entry
wenzelm@51534
    82
  {
wenzelm@51534
    83
    def timing: Double
wenzelm@51534
    84
    def print: String
wenzelm@51534
    85
    def follow(snapshot: Document.Snapshot)
wenzelm@51534
    86
  }
wenzelm@51534
    87
wenzelm@51536
    88
  private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
wenzelm@51536
    89
    extends Entry
wenzelm@51533
    90
  {
wenzelm@51534
    91
    def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
wenzelm@52980
    92
    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto(view, name.node) }
wenzelm@51534
    93
  }
wenzelm@51534
    94
wenzelm@51534
    95
  private case class Command_Entry(command: Command, timing: Double) extends Entry
wenzelm@51534
    96
  {
wenzelm@51534
    97
    def print: String = "  " + Time.print_seconds(timing) + "s command " + quote(command.name)
wenzelm@51533
    98
    def follow(snapshot: Document.Snapshot)
wenzelm@52980
    99
    { PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
wenzelm@51533
   100
  }
wenzelm@51533
   101
wenzelm@51533
   102
wenzelm@51533
   103
  /* timing view */
wenzelm@51533
   104
wenzelm@51533
   105
  private val timing_view = new ListView(Nil: List[Entry]) {
wenzelm@51533
   106
    listenTo(mouse.clicks)
wenzelm@51533
   107
    reactions += {
wenzelm@51533
   108
      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
wenzelm@51533
   109
        val index = peer.locationToIndex(point)
wenzelm@51533
   110
        if (index >= 0) listData(index).follow(PIDE.session.snapshot())
wenzelm@51533
   111
    }
wenzelm@51533
   112
  }
wenzelm@51533
   113
  timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
wenzelm@51533
   114
  timing_view.peer.setVisibleRowCount(0)
wenzelm@51533
   115
  timing_view.selection.intervalMode = ListView.IntervalMode.Single
wenzelm@51533
   116
  timing_view.renderer = new Entry.Renderer
wenzelm@51533
   117
wenzelm@51533
   118
  set_content(new ScrollPane(timing_view))
wenzelm@51533
   119
wenzelm@51533
   120
wenzelm@51533
   121
  /* timing threshold */
wenzelm@51533
   122
wenzelm@51533
   123
  private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
wenzelm@51533
   124
wenzelm@51549
   125
  private val threshold_tooltip = "Threshold for timing display (seconds)"
wenzelm@51549
   126
wenzelm@51549
   127
  private val threshold_label = new Label("Threshold: ") {
wenzelm@51549
   128
    tooltip = threshold_tooltip
wenzelm@51549
   129
  }
wenzelm@51533
   130
wenzelm@51533
   131
  private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
wenzelm@51533
   132
    reactions += {
wenzelm@51538
   133
      case _: ValueChanged =>
wenzelm@51533
   134
        text match {
wenzelm@51533
   135
          case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
wenzelm@51533
   136
          case _ =>
wenzelm@51533
   137
        }
wenzelm@51533
   138
        handle_update()
wenzelm@51533
   139
    }
wenzelm@51549
   140
    tooltip = threshold_tooltip
wenzelm@51538
   141
    verifier = ((s: String) =>
wenzelm@51538
   142
      s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
wenzelm@51533
   143
  }
wenzelm@51533
   144
wenzelm@51533
   145
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value)
wenzelm@51533
   146
  add(controls.peer, BorderLayout.NORTH)
wenzelm@51533
   147
wenzelm@51533
   148
wenzelm@51533
   149
  /* component state -- owned by Swing thread */
wenzelm@51533
   150
wenzelm@51533
   151
  private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
wenzelm@51534
   152
wenzelm@51534
   153
  private def make_entries(): List[Entry] =
wenzelm@51534
   154
  {
wenzelm@51534
   155
    Swing_Thread.require()
wenzelm@51534
   156
wenzelm@51534
   157
    val name =
wenzelm@51534
   158
      Document_View(view.getTextArea) match {
wenzelm@51534
   159
        case None => Document.Node.Name.empty
wenzelm@52973
   160
        case Some(doc_view) => doc_view.model.node_name
wenzelm@51534
   161
      }
wenzelm@52888
   162
    val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)
wenzelm@51534
   163
wenzelm@51534
   164
    val theories =
wenzelm@51536
   165
      (for ((node_name, node_timing) <- nodes_timing.toList if !node_timing.commands.isEmpty)
wenzelm@51536
   166
        yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
wenzelm@51534
   167
    val commands =
wenzelm@51534
   168
      (for ((command, command_timing) <- timing.commands.toList)
wenzelm@51534
   169
        yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
wenzelm@51534
   170
wenzelm@51536
   171
    theories.flatMap(entry =>
wenzelm@51536
   172
      if (entry.name == name) entry.copy(current = true) :: commands
wenzelm@51536
   173
      else List(entry))
wenzelm@51534
   174
  }
wenzelm@51533
   175
wenzelm@51533
   176
  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
wenzelm@51533
   177
  {
wenzelm@53177
   178
    Swing_Thread.require()
wenzelm@53177
   179
wenzelm@53177
   180
    val snapshot = PIDE.session.snapshot()
wenzelm@51533
   181
wenzelm@53177
   182
    val iterator =
wenzelm@53177
   183
      restriction match {
wenzelm@53177
   184
        case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
wenzelm@53177
   185
        case None => snapshot.version.nodes.entries
wenzelm@53177
   186
      }
wenzelm@53177
   187
    val nodes_timing1 =
wenzelm@53177
   188
      (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
wenzelm@53177
   189
          if (PIDE.thy_load.loaded_theories(name.theory)) timing1
wenzelm@53177
   190
          else {
wenzelm@53177
   191
            val node_timing =
wenzelm@53177
   192
              Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
wenzelm@53177
   193
            timing1 + (name -> node_timing)
wenzelm@53177
   194
          }
wenzelm@53177
   195
      })
wenzelm@53177
   196
    nodes_timing = nodes_timing1
wenzelm@51533
   197
wenzelm@53177
   198
    val entries = make_entries()
wenzelm@53177
   199
    if (timing_view.listData.toList != entries) timing_view.listData = entries
wenzelm@51533
   200
  }
wenzelm@51533
   201
wenzelm@51533
   202
wenzelm@51533
   203
  /* main actor */
wenzelm@51533
   204
wenzelm@51533
   205
  private val main_actor = actor {
wenzelm@51533
   206
    loop {
wenzelm@51533
   207
      react {
wenzelm@53177
   208
        case changed: Session.Commands_Changed =>
wenzelm@53177
   209
          Swing_Thread.later { handle_update(Some(changed.nodes)) }
wenzelm@51533
   210
wenzelm@51533
   211
        case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
wenzelm@51533
   212
      }
wenzelm@51533
   213
    }
wenzelm@51533
   214
  }
wenzelm@51533
   215
wenzelm@51533
   216
  override def init()
wenzelm@51533
   217
  {
wenzelm@51533
   218
    PIDE.session.commands_changed += main_actor
wenzelm@51533
   219
    handle_update()
wenzelm@51533
   220
  }
wenzelm@51533
   221
wenzelm@51533
   222
  override def exit()
wenzelm@51533
   223
  {
wenzelm@51533
   224
    PIDE.session.commands_changed -= main_actor
wenzelm@51533
   225
  }
wenzelm@51533
   226
}