--- a/NEWS Mon Mar 25 20:00:27 2013 +0100
+++ b/NEWS Tue Mar 26 11:26:13 2013 +0100
@@ -21,6 +21,12 @@
'ML_file' in Isabelle2013. Minor INCOMPATIBILITY.
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Dockable window "Timing" provides an overview of relevant command
+timing information.
+
+
*** Pure ***
* Discontinued obsolete 'axioms' command, which has been marked as
--- a/src/Pure/General/time.scala Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Pure/General/time.scala Tue Mar 26 11:26:13 2013 +0100
@@ -15,6 +15,9 @@
{
def seconds(s: Double): Time = new Time((s * 1000.0).round)
def ms(m: Long): Time = new Time(m)
+
+ def print_seconds(s: Double): String =
+ String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
}
final class Time private(val ms: Long)
@@ -26,8 +29,7 @@
def is_relevant: Boolean = ms >= 1
- override def toString =
- String.format(Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
+ override def toString = Time.print_seconds(seconds)
def message: String = toString + "s"
}
--- a/src/Pure/PIDE/protocol.scala Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Mar 26 11:26:13 2013 +0100
@@ -116,6 +116,36 @@
}
+ /* node timing */
+
+ sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
+
+ val empty_node_timing = Node_Timing(0.0, Map.empty)
+
+ def node_timing(
+ state: Document.State,
+ version: Document.Version,
+ node: Document.Node,
+ threshold: Double): Node_Timing =
+ {
+ var total = 0.0
+ var commands = Map.empty[Command, Double]
+ for {
+ command <- node.commands.iterator
+ st = state.command_state(version, command)
+ command_timing =
+ (0.0 /: st.status)({
+ case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
+ case (timing, _) => timing
+ })
+ } {
+ total += command_timing
+ if (command_timing >= threshold) commands += (command -> command_timing)
+ }
+ Node_Timing(total, commands)
+ }
+
+
/* result messages */
private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
--- a/src/Tools/jEdit/etc/options Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Tools/jEdit/etc/options Tue Mar 26 11:26:13 2013 +0100
@@ -27,6 +27,9 @@
option jedit_mac_adapter : bool = true
-- "some native Mac OS X support (potential conflict with MacOSX plugin)"
+option jedit_timing_threshold : real = 0.1
+ -- "default threshold for timing display"
+
section "Rendering of Document Content"
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Mar 26 11:26:13 2013 +0100
@@ -42,6 +42,7 @@
"src/syslog_dockable.scala"
"src/text_overview.scala"
"src/theories_dockable.scala"
+ "src/timing_dockable.scala"
"src/token_markup.scala"
)
--- a/src/Tools/jEdit/src/Isabelle.props Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Tue Mar 26 11:26:13 2013 +0100
@@ -37,7 +37,8 @@
isabelle.readme-panel \
isabelle.symbols-panel \
isabelle.syslog-panel \
- isabelle.theories-panel
+ isabelle.theories-panel \
+ isabelle.timing-panel
isabelle.monitor-panel.label=Monitor panel
isabelle.output-panel.label=Output panel
isabelle.protocol-panel.label=Protocol panel
@@ -46,6 +47,7 @@
isabelle.symbols-panel.label=Symbols panel
isabelle.syslog-panel.label=Syslog panel
isabelle.theories-panel.label=Theories panel
+isabelle.timing-panel.label=Timing panel
#dockables
isabelle-graphview.title=Graphview
@@ -58,6 +60,7 @@
isabelle-symbols.title=Symbols
isabelle-syslog.title=Syslog
isabelle-theories.title=Theories
+isabelle-timing.title=Timing
#SideKick
mode.isabelle-options.folding=sidekick
--- a/src/Tools/jEdit/src/actions.xml Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Tools/jEdit/src/actions.xml Tue Mar 26 11:26:13 2013 +0100
@@ -7,6 +7,11 @@
wm.addDockableWindow("isabelle-theories");
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.timing-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-timing");
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.syslog-panel">
<CODE>
wm.addDockableWindow("isabelle-syslog");
--- a/src/Tools/jEdit/src/dockables.xml Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Tools/jEdit/src/dockables.xml Tue Mar 26 11:26:13 2013 +0100
@@ -5,6 +5,9 @@
<DOCKABLE NAME="isabelle-theories" MOVABLE="TRUE">
new isabelle.jedit.Theories_Dockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-timing" MOVABLE="TRUE">
+ new isabelle.jedit.Timing_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
new isabelle.jedit.Syslog_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/src/isabelle.scala Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Mar 26 11:26:13 2013 +0100
@@ -26,6 +26,12 @@
case _ => None
}
+ def docked_timing(view: View): Option[Timing_Dockable] =
+ wm(view).getDockableWindow("isabelle-timing") match {
+ case dockable: Timing_Dockable => Some(dockable)
+ case _ => None
+ }
+
def docked_output(view: View): Option[Output_Dockable] =
wm(view).getDockableWindow("isabelle-output") match {
case dockable: Output_Dockable => Some(dockable)
--- a/src/Tools/jEdit/src/isabelle_options.scala Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Tue Mar 26 11:26:13 2013 +0100
@@ -43,10 +43,11 @@
private val relevant_options =
Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
"jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay",
- "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter", "threads",
- "threads_trace", "parallel_proofs", "parallel_subproofs_saturation", "editor_load_delay",
- "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
- "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
+ "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter",
+ "jedit_timing_threshold", "threads", "threads_trace", "parallel_proofs",
+ "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
+ "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
+ "editor_update_delay", "editor_chart_delay")
relevant_options.foreach(PIDE.options.value.check_name _)
--- /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
+ }
+}