more on Timing;
Sun, 03 Nov 2013 16:22:57 +0100
changeset 54359 e649dff217ae
parent 54358 0f50303e899f
child 54360 9d19298d3650
more on Timing;
--- a/src/Doc/JEdit/JEdit.thy	Fri Nov 01 17:26:47 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 03 16:22:57 2013 +0100
@@ -852,6 +852,34 @@
+section {* Timing *}
+text {* Managed evaluation of commands within PIDE documents includes
+  timing information, which consists of elapsed (wall-clock) time, CPU
+  time, and GC (garbage collection) time.  Note that in a
+  multithreaded system it is difficult to measure execution time
+  precisely: elapsed time is closer to the real requirements of
+  runtime resources than CPU or GC time, which are both subject to
+  influences from the parallel environment that are outside the scope
+  of the current command transaction.
+  The \emph{Timing} panel provides an overview of cumulative command
+  timings for each document node.  Commands with elapsed time below
+  the given threshold are ignored in the grand total.  Nodes are
+  sorted according to their overall timing.  For the document node
+  that corresponds to the current buffer, individual command timings
+  are shown as well.  A double-click on a theory node or command moves
+  the editor focus to that particular source position.
+  It is also possible to reveal individual timing information via some
+  tooltip for the corresponding command keyword, using the technique
+  of mouse hovering with @{verbatim CONTROL}/@{verbatim COMMAND}
+  modifier key as explained in \secref{sec:tooltips-hyperlinks}.
+  Actual display of timing depends on the global option
+  @{system_option jedit_timing_threshold}, which can be configured in
+  "Plugin Options / Isabelle / General".  *}
 section {* Isabelle/Scala console *}
 text {* The \emph{Console} plugin of jEdit manages various shells