src/Tools/jEdit/src/timing_dockable.scala
author wenzelm
Tue Mar 26 12:40:51 2013 +0100 (2013-03-26)
changeset 51534 123bd97fcea1
parent 51533 3f6280aedbcc
child 51536 a1d324ef12d4
permissions -rw-r--r--
mixed theory/command entries;
tuned;
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@51533
    14
import scala.swing.event.{EditDone, MouseClicked}
wenzelm@51533
    15
wenzelm@51533
    16
import java.lang.System
wenzelm@51533
    17
import java.awt.{BorderLayout, Graphics2D, Insets}
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@51533
    41
    }
wenzelm@51533
    42
wenzelm@51533
    43
    class Renderer extends ListView.Renderer[Entry]
wenzelm@51533
    44
    {
wenzelm@51533
    45
      def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
wenzelm@51533
    46
        entry: Entry, index: Int): Component =
wenzelm@51533
    47
      {
wenzelm@51533
    48
        val component = Renderer_Component
wenzelm@51534
    49
        component.text = entry.print
wenzelm@51533
    50
        component
wenzelm@51533
    51
      }
wenzelm@51533
    52
    }
wenzelm@51533
    53
  }
wenzelm@51533
    54
wenzelm@51534
    55
  private abstract class Entry
wenzelm@51534
    56
  {
wenzelm@51534
    57
    def timing: Double
wenzelm@51534
    58
    def print: String
wenzelm@51534
    59
    def follow(snapshot: Document.Snapshot)
wenzelm@51534
    60
  }
wenzelm@51534
    61
wenzelm@51534
    62
  private case class Theory_Entry(name: Document.Node.Name, timing: Double) extends Entry
wenzelm@51533
    63
  {
wenzelm@51534
    64
    def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
wenzelm@51534
    65
    def follow(snapshot: Document.Snapshot): Unit = Hyperlink(name.node).follow(view)
wenzelm@51534
    66
  }
wenzelm@51534
    67
wenzelm@51534
    68
  private case class Command_Entry(command: Command, timing: Double) extends Entry
wenzelm@51534
    69
  {
wenzelm@51534
    70
    def print: String = "  " + Time.print_seconds(timing) + "s command " + quote(command.name)
wenzelm@51534
    71
wenzelm@51533
    72
    def follow(snapshot: Document.Snapshot)
wenzelm@51533
    73
    {
wenzelm@51533
    74
      val node = snapshot.version.nodes(command.node_name)
wenzelm@51533
    75
      if (node.commands.contains(command)) {
wenzelm@51533
    76
        val sources = node.commands.iterator.takeWhile(_ != command).map(_.source)
wenzelm@51533
    77
        val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
wenzelm@51533
    78
        Hyperlink(command.node_name.node, line, column).follow(view)
wenzelm@51533
    79
      }
wenzelm@51533
    80
    }
wenzelm@51533
    81
  }
wenzelm@51533
    82
wenzelm@51533
    83
wenzelm@51533
    84
  /* timing view */
wenzelm@51533
    85
wenzelm@51533
    86
  private val timing_view = new ListView(Nil: List[Entry]) {
wenzelm@51533
    87
    listenTo(mouse.clicks)
wenzelm@51533
    88
    reactions += {
wenzelm@51533
    89
      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
wenzelm@51533
    90
        val index = peer.locationToIndex(point)
wenzelm@51533
    91
        if (index >= 0) listData(index).follow(PIDE.session.snapshot())
wenzelm@51533
    92
    }
wenzelm@51533
    93
  }
wenzelm@51533
    94
  timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
wenzelm@51533
    95
  timing_view.peer.setVisibleRowCount(0)
wenzelm@51533
    96
  timing_view.selection.intervalMode = ListView.IntervalMode.Single
wenzelm@51533
    97
  timing_view.renderer = new Entry.Renderer
wenzelm@51533
    98
wenzelm@51533
    99
  set_content(new ScrollPane(timing_view))
wenzelm@51533
   100
wenzelm@51533
   101
wenzelm@51533
   102
  /* timing threshold */
wenzelm@51533
   103
wenzelm@51533
   104
  private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
wenzelm@51533
   105
wenzelm@51534
   106
  private val threshold_label = new Label("Threshold: ")
wenzelm@51533
   107
wenzelm@51533
   108
  private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
wenzelm@51533
   109
    reactions += {
wenzelm@51533
   110
      case EditDone(_) =>
wenzelm@51533
   111
        text match {
wenzelm@51533
   112
          case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
wenzelm@51533
   113
          case _ =>
wenzelm@51533
   114
        }
wenzelm@51533
   115
        text = Time.print_seconds(timing_threshold)
wenzelm@51533
   116
        handle_update()
wenzelm@51533
   117
    }
wenzelm@51533
   118
    tooltip = "Threshold for timing display (seconds)"
wenzelm@51533
   119
  }
wenzelm@51533
   120
wenzelm@51533
   121
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value)
wenzelm@51533
   122
  add(controls.peer, BorderLayout.NORTH)
wenzelm@51533
   123
wenzelm@51533
   124
wenzelm@51533
   125
  /* component state -- owned by Swing thread */
wenzelm@51533
   126
wenzelm@51533
   127
  private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
wenzelm@51534
   128
wenzelm@51534
   129
  private def make_entries(): List[Entry] =
wenzelm@51534
   130
  {
wenzelm@51534
   131
    Swing_Thread.require()
wenzelm@51534
   132
wenzelm@51534
   133
    val name =
wenzelm@51534
   134
      Document_View(view.getTextArea) match {
wenzelm@51534
   135
        case None => Document.Node.Name.empty
wenzelm@51534
   136
        case Some(doc_view) => doc_view.model.name
wenzelm@51534
   137
      }
wenzelm@51534
   138
    val timing = nodes_timing.get(name) getOrElse Protocol.empty_node_timing
wenzelm@51534
   139
wenzelm@51534
   140
    val theories =
wenzelm@51534
   141
      (for {
wenzelm@51534
   142
        (node_name, node_timing) <- nodes_timing.toList
wenzelm@51534
   143
        if node_timing.total > timing_threshold
wenzelm@51534
   144
      } yield Theory_Entry(node_name, node_timing.total)).sorted(Entry.Ordering)
wenzelm@51534
   145
    val commands =
wenzelm@51534
   146
      (for ((command, command_timing) <- timing.commands.toList)
wenzelm@51534
   147
        yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
wenzelm@51534
   148
wenzelm@51534
   149
    theories.flatMap(entry => entry :: (if (entry.name == name) commands else Nil))
wenzelm@51534
   150
  }
wenzelm@51533
   151
wenzelm@51533
   152
  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
wenzelm@51533
   153
  {
wenzelm@51533
   154
    Swing_Thread.now {
wenzelm@51533
   155
      val snapshot = PIDE.session.snapshot()
wenzelm@51533
   156
wenzelm@51533
   157
      val iterator =
wenzelm@51533
   158
        restriction match {
wenzelm@51533
   159
          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
wenzelm@51533
   160
          case None => snapshot.version.nodes.entries
wenzelm@51533
   161
        }
wenzelm@51533
   162
      val nodes_timing1 =
wenzelm@51533
   163
        (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
wenzelm@51533
   164
            if (PIDE.thy_load.loaded_theories(name.theory)) timing1
wenzelm@51533
   165
            else {
wenzelm@51533
   166
              val node_timing =
wenzelm@51533
   167
                Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
wenzelm@51533
   168
              timing1 + (name -> node_timing)
wenzelm@51533
   169
            }
wenzelm@51533
   170
        })
wenzelm@51533
   171
      nodes_timing = nodes_timing1
wenzelm@51533
   172
wenzelm@51534
   173
      val entries = make_entries()
wenzelm@51534
   174
      if (timing_view.listData.toList != entries) timing_view.listData = entries
wenzelm@51533
   175
    }
wenzelm@51533
   176
  }
wenzelm@51533
   177
wenzelm@51533
   178
wenzelm@51533
   179
  /* main actor */
wenzelm@51533
   180
wenzelm@51533
   181
  private val main_actor = actor {
wenzelm@51533
   182
    loop {
wenzelm@51533
   183
      react {
wenzelm@51533
   184
        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
wenzelm@51533
   185
wenzelm@51533
   186
        case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
wenzelm@51533
   187
      }
wenzelm@51533
   188
    }
wenzelm@51533
   189
  }
wenzelm@51533
   190
wenzelm@51533
   191
  override def init()
wenzelm@51533
   192
  {
wenzelm@51533
   193
    PIDE.session.commands_changed += main_actor
wenzelm@51533
   194
    handle_update()
wenzelm@51533
   195
  }
wenzelm@51533
   196
wenzelm@51533
   197
  override def exit()
wenzelm@51533
   198
  {
wenzelm@51533
   199
    PIDE.session.commands_changed -= main_actor
wenzelm@51533
   200
  }
wenzelm@51533
   201
}