# HG changeset patch
# User wenzelm
# Date 1383492177 -3600
# Node ID e649dff217ae446d0507465b4a9f53d21cad3ae5
# Parent  0f50303e899f2e842eb392648e460cf104dda3a0
more on Timing;

diff -r 0f50303e899f -r e649dff217ae src/Doc/JEdit/JEdit.thy
--- 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