# 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 + } +}