# HG changeset patch
# User wenzelm
# Date 1364307028 -3600
# Node ID 625d2ec0bbff41dac9e55f2c314c8ce6dd7c9f31
# Parent 637e64effda2fbd4f58b488fe62468dc0cab79f3# Parent cdffeaf1402ec98feaa4ba7bf963c958c8cc3441
merged
diff -r cdffeaf1402e -r 625d2ec0bbff NEWS
--- a/NEWS Tue Mar 26 13:54:24 2013 +0100
+++ b/NEWS Tue Mar 26 15:10:28 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
diff -r cdffeaf1402e -r 625d2ec0bbff src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Mar 26 13:54:24 2013 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Mar 26 15:10:28 2013 +0100
@@ -3,7 +3,7 @@
header{*Fundamental Theorem of Algebra*}
theory Fundamental_Theorem_Algebra
-imports Polynomial Complex
+imports Polynomial Complex_Main
begin
subsection {* Square root of complex numbers *}
diff -r cdffeaf1402e -r 625d2ec0bbff src/HOL/Real.thy
diff -r cdffeaf1402e -r 625d2ec0bbff src/Pure/General/time.scala
--- a/src/Pure/General/time.scala Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Pure/General/time.scala Tue Mar 26 15:10:28 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"
}
diff -r cdffeaf1402e -r 625d2ec0bbff src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Mar 26 15:10:28 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)
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Tools/jEdit/etc/options Tue Mar 26 15:10:28 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"
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Mar 26 15:10:28 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"
)
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Tue Mar 26 15:10:28 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
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Tools/jEdit/src/actions.xml Tue Mar 26 15:10:28 2013 +0100
@@ -7,6 +7,11 @@
wm.addDockableWindow("isabelle-theories");
+
+
+ wm.addDockableWindow("isabelle-timing");
+
+
wm.addDockableWindow("isabelle-syslog");
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/src/dockables.xml
--- a/src/Tools/jEdit/src/dockables.xml Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Tools/jEdit/src/dockables.xml Tue Mar 26 15:10:28 2013 +0100
@@ -5,6 +5,9 @@
new isabelle.jedit.Theories_Dockable(view, position);
+
+ new isabelle.jedit.Timing_Dockable(view, position);
+
new isabelle.jedit.Syslog_Dockable(view, position);
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/src/hyperlink.scala
--- a/src/Tools/jEdit/src/hyperlink.scala Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Tools/jEdit/src/hyperlink.scala Tue Mar 26 15:10:28 2013 +0100
@@ -16,7 +16,7 @@
object Hyperlink
{
- def apply(jedit_file: String, line: Int, column: Int): Hyperlink =
+ def apply(jedit_file: String, line: Int = 0, column: Int = 0): Hyperlink =
File_Link(jedit_file, line, column)
}
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Mar 26 15:10:28 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)
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Tue Mar 26 15:10:28 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 _)
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 26 13:54:24 2013 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 26 15:10:28 2013 +0100
@@ -30,7 +30,7 @@
reactions += {
case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
val index = peer.locationToIndex(point)
- if (index >= 0) jEdit.openFile(view, listData(index).node)
+ if (index >= 0) Hyperlink(listData(index).node).follow(view)
}
}
status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
@@ -93,7 +93,7 @@
(st.failed, PIDE.options.color_value("error_color")))
val size = peer.getSize()
- val insets = border.getBorderInsets(this.peer)
+ val insets = border.getBorderInsets(peer)
val w = size.width - insets.left - insets.right
val h = size.height - insets.top - insets.bottom
var end = size.width - insets.right
diff -r cdffeaf1402e -r 625d2ec0bbff src/Tools/jEdit/src/timing_dockable.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Mar 26 15:10:28 2013 +0100
@@ -0,0 +1,229 @@
+/* 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.{MouseClicked, ValueChanged}
+
+import java.lang.System
+import java.awt.{BorderLayout, Graphics2D, Insets, Color}
+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)
+
+ var entry: Entry = null
+ override def paintComponent(gfx: Graphics2D)
+ {
+ def paint_rectangle(color: Color)
+ {
+ val size = peer.getSize()
+ val insets = border.getBorderInsets(peer)
+ val x = insets.left
+ val y = insets.top
+ val w = size.width - x - insets.right
+ val h = size.height - y - insets.bottom
+ gfx.setColor(color)
+ gfx.fillRect(x, y, w, h)
+ }
+
+ entry match {
+ case theory_entry: Theory_Entry if theory_entry.current =>
+ paint_rectangle(view.getTextArea.getPainter.getSelectionColor)
+ case _: Command_Entry =>
+ paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor)
+ case _ =>
+ }
+ super.paintComponent(gfx)
+ }
+ }
+
+ class Renderer extends ListView.Renderer[Entry]
+ {
+ def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
+ entry: Entry, index: Int): Component =
+ {
+ val component = Renderer_Component
+ component.entry = entry
+ component.text = entry.print
+ component
+ }
+ }
+ }
+
+ private abstract class Entry
+ {
+ def timing: Double
+ def print: String
+ def follow(snapshot: Document.Snapshot)
+ }
+
+ private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
+ extends Entry
+ {
+ def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
+ def follow(snapshot: Document.Snapshot): Unit = Hyperlink(name.node).follow(view)
+ }
+
+ private case class Command_Entry(command: Command, timing: Double) extends Entry
+ {
+ def print: String = " " + Time.print_seconds(timing) + "s command " + quote(command.name)
+
+ 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("Threshold: ")
+
+ private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
+ reactions += {
+ case _: ValueChanged =>
+ text match {
+ case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
+ case _ =>
+ }
+ handle_update()
+ }
+ tooltip = "Threshold for timing display (seconds)"
+ verifier = ((s: String) =>
+ s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
+ }
+
+ 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 def make_entries(): List[Entry] =
+ {
+ Swing_Thread.require()
+
+ val name =
+ Document_View(view.getTextArea) match {
+ case None => Document.Node.Name.empty
+ case Some(doc_view) => doc_view.model.name
+ }
+ val timing = nodes_timing.get(name) getOrElse Protocol.empty_node_timing
+
+ val theories =
+ (for ((node_name, node_timing) <- nodes_timing.toList if !node_timing.commands.isEmpty)
+ yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
+ val commands =
+ (for ((command, command_timing) <- timing.commands.toList)
+ yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
+
+ theories.flatMap(entry =>
+ if (entry.name == name) entry.copy(current = true) :: commands
+ else List(entry))
+ }
+
+ 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
+
+ val entries = make_entries()
+ if (timing_view.listData.toList != entries) timing_view.listData = entries
+ }
+ }
+
+
+ /* 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
+ }
+}