--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Mar 26 11:26:13 2013 +0100
@@ -0,0 +1,175 @@
+/* Title: Tools/jEdit/src/timing_dockable.scala
+ Author: Makarius
+
+Dockable window for timing information.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+import scala.swing.{FlowPanel, Label, ListView, Alignment, ScrollPane, Component, TextField}
+import scala.swing.event.{EditDone, MouseClicked}
+
+import java.lang.System
+import java.awt.{BorderLayout, Graphics2D, Insets}
+import javax.swing.{JList, BorderFactory}
+import javax.swing.border.{BevelBorder, SoftBevelBorder}
+
+import org.gjt.sp.jedit.{View, jEdit}
+
+
+class Timing_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ /* entry */
+
+ private object Entry
+ {
+ object Ordering extends scala.math.Ordering[Entry]
+ {
+ def compare(entry1: Entry, entry2: Entry): Int =
+ entry2.timing compare entry1.timing
+ }
+
+ object Renderer_Component extends Label
+ {
+ opaque = false
+ xAlignment = Alignment.Leading
+ border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
+ }
+
+ class Renderer extends ListView.Renderer[Entry]
+ {
+ def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
+ entry: Entry, index: Int): Component =
+ {
+ val component = Renderer_Component
+ component.text = Time.print_seconds(entry.timing) + "s " + entry.command.name
+ component
+ }
+ }
+ }
+
+ private case class Entry(command: Command, timing: Double)
+ {
+ def follow(snapshot: Document.Snapshot)
+ {
+ val node = snapshot.version.nodes(command.node_name)
+ if (node.commands.contains(command)) {
+ val sources = node.commands.iterator.takeWhile(_ != command).map(_.source)
+ val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+ Hyperlink(command.node_name.node, line, column).follow(view)
+ }
+ }
+ }
+
+
+ /* timing view */
+
+ private val timing_view = new ListView(Nil: List[Entry]) {
+ listenTo(mouse.clicks)
+ reactions += {
+ case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
+ val index = peer.locationToIndex(point)
+ if (index >= 0) listData(index).follow(PIDE.session.snapshot())
+ }
+ }
+ timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
+ timing_view.peer.setVisibleRowCount(0)
+ timing_view.selection.intervalMode = ListView.IntervalMode.Single
+ timing_view.renderer = new Entry.Renderer
+
+ set_content(new ScrollPane(timing_view))
+
+
+ /* timing threshold */
+
+ private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
+
+ private val threshold_label = new Label("Timing threshold: ")
+
+ private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
+ reactions += {
+ case EditDone(_) =>
+ text match {
+ case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
+ case _ =>
+ }
+ text = Time.print_seconds(timing_threshold)
+ handle_update()
+ }
+ tooltip = "Threshold for timing display (seconds)"
+ }
+
+ private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value)
+ add(controls.peer, BorderLayout.NORTH)
+
+
+ /* component state -- owned by Swing thread */
+
+ private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
+ private var current_name = Document.Node.Name.empty
+ private var current_timing = Protocol.empty_node_timing
+
+ private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
+ {
+ Swing_Thread.now {
+ val snapshot = PIDE.session.snapshot()
+
+ val iterator =
+ restriction match {
+ case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
+ case None => snapshot.version.nodes.entries
+ }
+ val nodes_timing1 =
+ (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
+ if (PIDE.thy_load.loaded_theories(name.theory)) timing1
+ else {
+ val node_timing =
+ Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
+ timing1 + (name -> node_timing)
+ }
+ })
+ nodes_timing = nodes_timing1
+
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ val name = doc_view.model.name
+ val timing = nodes_timing.get(name) getOrElse Protocol.empty_node_timing
+ if (current_name != name || current_timing != timing) {
+ current_name = name
+ current_timing = timing
+ timing_view.listData =
+ timing.commands.toList.map(p => Entry(p._1, p._2)).sorted(Entry.Ordering)
+ }
+ case None =>
+ }
+ }
+ }
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
+
+ case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ PIDE.session.commands_changed += main_actor
+ handle_update()
+ }
+
+ override def exit()
+ {
+ PIDE.session.commands_changed -= main_actor
+ }
+}