dockable window for timing information;
authorwenzelm
Tue Mar 26 11:26:13 2013 +0100 (2013-03-26)
changeset 515333f6280aedbcc
parent 51517 7957d26c3334
child 51534 123bd97fcea1
dockable window for timing information;
NEWS
src/Pure/General/time.scala
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/dockables.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/NEWS	Mon Mar 25 20:00:27 2013 +0100
     1.2 +++ b/NEWS	Tue Mar 26 11:26:13 2013 +0100
     1.3 @@ -21,6 +21,12 @@
     1.4  'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.
     1.5  
     1.6  
     1.7 +*** Prover IDE -- Isabelle/Scala/jEdit ***
     1.8 +
     1.9 +* Dockable window "Timing" provides an overview of relevant command
    1.10 +timing information.
    1.11 +
    1.12 +
    1.13  *** Pure ***
    1.14  
    1.15  * Discontinued obsolete 'axioms' command, which has been marked as
     2.1 --- a/src/Pure/General/time.scala	Mon Mar 25 20:00:27 2013 +0100
     2.2 +++ b/src/Pure/General/time.scala	Tue Mar 26 11:26:13 2013 +0100
     2.3 @@ -15,6 +15,9 @@
     2.4  {
     2.5    def seconds(s: Double): Time = new Time((s * 1000.0).round)
     2.6    def ms(m: Long): Time = new Time(m)
     2.7 +
     2.8 +  def print_seconds(s: Double): String =
     2.9 +    String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    2.10  }
    2.11  
    2.12  final class Time private(val ms: Long)
    2.13 @@ -26,8 +29,7 @@
    2.14  
    2.15    def is_relevant: Boolean = ms >= 1
    2.16  
    2.17 -  override def toString =
    2.18 -    String.format(Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
    2.19 +  override def toString = Time.print_seconds(seconds)
    2.20  
    2.21    def message: String = toString + "s"
    2.22  }
     3.1 --- a/src/Pure/PIDE/protocol.scala	Mon Mar 25 20:00:27 2013 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Mar 26 11:26:13 2013 +0100
     3.3 @@ -116,6 +116,36 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* node timing */
     3.8 +
     3.9 +  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
    3.10 +
    3.11 +  val empty_node_timing = Node_Timing(0.0, Map.empty)
    3.12 +
    3.13 +  def node_timing(
    3.14 +    state: Document.State,
    3.15 +    version: Document.Version,
    3.16 +    node: Document.Node,
    3.17 +    threshold: Double): Node_Timing =
    3.18 +  {
    3.19 +    var total = 0.0
    3.20 +    var commands = Map.empty[Command, Double]
    3.21 +    for {
    3.22 +      command <- node.commands.iterator
    3.23 +      st = state.command_state(version, command)
    3.24 +      command_timing =
    3.25 +        (0.0 /: st.status)({
    3.26 +          case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
    3.27 +          case (timing, _) => timing
    3.28 +        })
    3.29 +    } {
    3.30 +      total += command_timing
    3.31 +      if (command_timing >= threshold) commands += (command -> command_timing)
    3.32 +    }
    3.33 +    Node_Timing(total, commands)
    3.34 +  }
    3.35 +
    3.36 +
    3.37    /* result messages */
    3.38  
    3.39    private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
     4.1 --- a/src/Tools/jEdit/etc/options	Mon Mar 25 20:00:27 2013 +0100
     4.2 +++ b/src/Tools/jEdit/etc/options	Tue Mar 26 11:26:13 2013 +0100
     4.3 @@ -27,6 +27,9 @@
     4.4  option jedit_mac_adapter : bool = true
     4.5    -- "some native Mac OS X support (potential conflict with MacOSX plugin)"
     4.6  
     4.7 +option jedit_timing_threshold : real = 0.1
     4.8 +  -- "default threshold for timing display"
     4.9 +
    4.10  
    4.11  section "Rendering of Document Content"
    4.12  
     5.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Mar 25 20:00:27 2013 +0100
     5.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 26 11:26:13 2013 +0100
     5.3 @@ -42,6 +42,7 @@
     5.4    "src/syslog_dockable.scala"
     5.5    "src/text_overview.scala"
     5.6    "src/theories_dockable.scala"
     5.7 +  "src/timing_dockable.scala"
     5.8    "src/token_markup.scala"
     5.9  )
    5.10  
     6.1 --- a/src/Tools/jEdit/src/Isabelle.props	Mon Mar 25 20:00:27 2013 +0100
     6.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Tue Mar 26 11:26:13 2013 +0100
     6.3 @@ -37,7 +37,8 @@
     6.4    isabelle.readme-panel \
     6.5    isabelle.symbols-panel \
     6.6    isabelle.syslog-panel \
     6.7 -  isabelle.theories-panel
     6.8 +  isabelle.theories-panel \
     6.9 +  isabelle.timing-panel
    6.10  isabelle.monitor-panel.label=Monitor panel
    6.11  isabelle.output-panel.label=Output panel
    6.12  isabelle.protocol-panel.label=Protocol panel
    6.13 @@ -46,6 +47,7 @@
    6.14  isabelle.symbols-panel.label=Symbols panel
    6.15  isabelle.syslog-panel.label=Syslog panel
    6.16  isabelle.theories-panel.label=Theories panel
    6.17 +isabelle.timing-panel.label=Timing panel
    6.18  
    6.19  #dockables
    6.20  isabelle-graphview.title=Graphview
    6.21 @@ -58,6 +60,7 @@
    6.22  isabelle-symbols.title=Symbols
    6.23  isabelle-syslog.title=Syslog
    6.24  isabelle-theories.title=Theories
    6.25 +isabelle-timing.title=Timing
    6.26  
    6.27  #SideKick
    6.28  mode.isabelle-options.folding=sidekick
     7.1 --- a/src/Tools/jEdit/src/actions.xml	Mon Mar 25 20:00:27 2013 +0100
     7.2 +++ b/src/Tools/jEdit/src/actions.xml	Tue Mar 26 11:26:13 2013 +0100
     7.3 @@ -7,6 +7,11 @@
     7.4  			wm.addDockableWindow("isabelle-theories");
     7.5  		</CODE>
     7.6  	</ACTION>
     7.7 +	<ACTION NAME="isabelle.timing-panel">
     7.8 +		<CODE>
     7.9 +			wm.addDockableWindow("isabelle-timing");
    7.10 +		</CODE>
    7.11 +	</ACTION>
    7.12  	<ACTION NAME="isabelle.syslog-panel">
    7.13  		<CODE>
    7.14  			wm.addDockableWindow("isabelle-syslog");
     8.1 --- a/src/Tools/jEdit/src/dockables.xml	Mon Mar 25 20:00:27 2013 +0100
     8.2 +++ b/src/Tools/jEdit/src/dockables.xml	Tue Mar 26 11:26:13 2013 +0100
     8.3 @@ -5,6 +5,9 @@
     8.4  	<DOCKABLE NAME="isabelle-theories" MOVABLE="TRUE">
     8.5  		new isabelle.jedit.Theories_Dockable(view, position);
     8.6  	</DOCKABLE>
     8.7 +	<DOCKABLE NAME="isabelle-timing" MOVABLE="TRUE">
     8.8 +		new isabelle.jedit.Timing_Dockable(view, position);
     8.9 +	</DOCKABLE>
    8.10  	<DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
    8.11  		new isabelle.jedit.Syslog_Dockable(view, position);
    8.12  	</DOCKABLE>
     9.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Mar 25 20:00:27 2013 +0100
     9.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 26 11:26:13 2013 +0100
     9.3 @@ -26,6 +26,12 @@
     9.4        case _ => None
     9.5      }
     9.6  
     9.7 +  def docked_timing(view: View): Option[Timing_Dockable] =
     9.8 +    wm(view).getDockableWindow("isabelle-timing") match {
     9.9 +      case dockable: Timing_Dockable => Some(dockable)
    9.10 +      case _ => None
    9.11 +    }
    9.12 +
    9.13    def docked_output(view: View): Option[Output_Dockable] =
    9.14      wm(view).getDockableWindow("isabelle-output") match {
    9.15        case dockable: Output_Dockable => Some(dockable)
    10.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Mon Mar 25 20:00:27 2013 +0100
    10.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Mar 26 11:26:13 2013 +0100
    10.3 @@ -43,10 +43,11 @@
    10.4    private val relevant_options =
    10.5      Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
    10.6        "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay",
    10.7 -      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter", "threads",
    10.8 -      "threads_trace", "parallel_proofs", "parallel_subproofs_saturation", "editor_load_delay",
    10.9 -      "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
   10.10 -      "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
   10.11 +      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter",
   10.12 +      "jedit_timing_threshold", "threads", "threads_trace", "parallel_proofs",
   10.13 +      "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
   10.14 +      "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
   10.15 +      "editor_update_delay", "editor_chart_delay")
   10.16  
   10.17    relevant_options.foreach(PIDE.options.value.check_name _)
   10.18  
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 26 11:26:13 2013 +0100
    11.3 @@ -0,0 +1,175 @@
    11.4 +/*  Title:      Tools/jEdit/src/timing_dockable.scala
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Dockable window for timing information.
    11.8 +*/
    11.9 +
   11.10 +package isabelle.jedit
   11.11 +
   11.12 +
   11.13 +import isabelle._
   11.14 +
   11.15 +import scala.actors.Actor._
   11.16 +import scala.swing.{FlowPanel, Label, ListView, Alignment, ScrollPane, Component, TextField}
   11.17 +import scala.swing.event.{EditDone, MouseClicked}
   11.18 +
   11.19 +import java.lang.System
   11.20 +import java.awt.{BorderLayout, Graphics2D, Insets}
   11.21 +import javax.swing.{JList, BorderFactory}
   11.22 +import javax.swing.border.{BevelBorder, SoftBevelBorder}
   11.23 +
   11.24 +import org.gjt.sp.jedit.{View, jEdit}
   11.25 +
   11.26 +
   11.27 +class Timing_Dockable(view: View, position: String) extends Dockable(view, position)
   11.28 +{
   11.29 +  /* entry */
   11.30 +
   11.31 +  private object Entry
   11.32 +  {
   11.33 +    object Ordering extends scala.math.Ordering[Entry]
   11.34 +    {
   11.35 +      def compare(entry1: Entry, entry2: Entry): Int =
   11.36 +        entry2.timing compare entry1.timing
   11.37 +    }
   11.38 +
   11.39 +    object Renderer_Component extends Label
   11.40 +    {
   11.41 +      opaque = false
   11.42 +      xAlignment = Alignment.Leading
   11.43 +      border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
   11.44 +    }
   11.45 +
   11.46 +    class Renderer extends ListView.Renderer[Entry]
   11.47 +    {
   11.48 +      def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
   11.49 +        entry: Entry, index: Int): Component =
   11.50 +      {
   11.51 +        val component = Renderer_Component
   11.52 +        component.text = Time.print_seconds(entry.timing) + "s " + entry.command.name
   11.53 +        component
   11.54 +      }
   11.55 +    }
   11.56 +  }
   11.57 +
   11.58 +  private case class Entry(command: Command, timing: Double)
   11.59 +  {
   11.60 +    def follow(snapshot: Document.Snapshot)
   11.61 +    {
   11.62 +      val node = snapshot.version.nodes(command.node_name)
   11.63 +      if (node.commands.contains(command)) {
   11.64 +        val sources = node.commands.iterator.takeWhile(_ != command).map(_.source)
   11.65 +        val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   11.66 +        Hyperlink(command.node_name.node, line, column).follow(view)
   11.67 +      }
   11.68 +    }
   11.69 +  }
   11.70 +
   11.71 +
   11.72 +  /* timing view */
   11.73 +
   11.74 +  private val timing_view = new ListView(Nil: List[Entry]) {
   11.75 +    listenTo(mouse.clicks)
   11.76 +    reactions += {
   11.77 +      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
   11.78 +        val index = peer.locationToIndex(point)
   11.79 +        if (index >= 0) listData(index).follow(PIDE.session.snapshot())
   11.80 +    }
   11.81 +  }
   11.82 +  timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
   11.83 +  timing_view.peer.setVisibleRowCount(0)
   11.84 +  timing_view.selection.intervalMode = ListView.IntervalMode.Single
   11.85 +  timing_view.renderer = new Entry.Renderer
   11.86 +
   11.87 +  set_content(new ScrollPane(timing_view))
   11.88 +
   11.89 +
   11.90 +  /* timing threshold */
   11.91 +
   11.92 +  private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
   11.93 +
   11.94 +  private val threshold_label = new Label("Timing threshold: ")
   11.95 +
   11.96 +  private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
   11.97 +    reactions += {
   11.98 +      case EditDone(_) =>
   11.99 +        text match {
  11.100 +          case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
  11.101 +          case _ =>
  11.102 +        }
  11.103 +        text = Time.print_seconds(timing_threshold)
  11.104 +        handle_update()
  11.105 +    }
  11.106 +    tooltip = "Threshold for timing display (seconds)"
  11.107 +  }
  11.108 +
  11.109 +  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value)
  11.110 +  add(controls.peer, BorderLayout.NORTH)
  11.111 +
  11.112 +
  11.113 +  /* component state -- owned by Swing thread */
  11.114 +
  11.115 +  private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
  11.116 +  private var current_name = Document.Node.Name.empty
  11.117 +  private var current_timing = Protocol.empty_node_timing
  11.118 +
  11.119 +  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
  11.120 +  {
  11.121 +    Swing_Thread.now {
  11.122 +      val snapshot = PIDE.session.snapshot()
  11.123 +
  11.124 +      val iterator =
  11.125 +        restriction match {
  11.126 +          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
  11.127 +          case None => snapshot.version.nodes.entries
  11.128 +        }
  11.129 +      val nodes_timing1 =
  11.130 +        (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
  11.131 +            if (PIDE.thy_load.loaded_theories(name.theory)) timing1
  11.132 +            else {
  11.133 +              val node_timing =
  11.134 +                Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
  11.135 +              timing1 + (name -> node_timing)
  11.136 +            }
  11.137 +        })
  11.138 +      nodes_timing = nodes_timing1
  11.139 +
  11.140 +      Document_View(view.getTextArea) match {
  11.141 +        case Some(doc_view) =>
  11.142 +          val name = doc_view.model.name
  11.143 +          val timing = nodes_timing.get(name) getOrElse Protocol.empty_node_timing
  11.144 +          if (current_name != name || current_timing != timing) {
  11.145 +            current_name = name
  11.146 +            current_timing = timing
  11.147 +            timing_view.listData =
  11.148 +              timing.commands.toList.map(p => Entry(p._1, p._2)).sorted(Entry.Ordering)
  11.149 +          }
  11.150 +        case None =>
  11.151 +      }
  11.152 +    }
  11.153 +  }
  11.154 +
  11.155 +
  11.156 +  /* main actor */
  11.157 +
  11.158 +  private val main_actor = actor {
  11.159 +    loop {
  11.160 +      react {
  11.161 +        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
  11.162 +
  11.163 +        case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
  11.164 +      }
  11.165 +    }
  11.166 +  }
  11.167 +
  11.168 +  override def init()
  11.169 +  {
  11.170 +    PIDE.session.commands_changed += main_actor
  11.171 +    handle_update()
  11.172 +  }
  11.173 +
  11.174 +  override def exit()
  11.175 +  {
  11.176 +    PIDE.session.commands_changed -= main_actor
  11.177 +  }
  11.178 +}