# HG changeset patch
# User wenzelm
# Date 1405948610 -7200
# Node ID 06cb5375e1898edda350af96b0013a89baae3c8f
# Parent  e0e4ac981cf1170278cd739b9125509c8ca30c33
more on "Simplifier trace" (by Lars Hupel);

diff -r e0e4ac981cf1 -r 06cb5375e189 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 14:24:10 2014 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 15:16:50 2014 +0200
@@ -893,6 +893,54 @@
   \end{description}
 *}
 
+subsection {* Simplifier trace \label{sec:simplifier-trace} *}
+
+text {*
+  The new visual tracing facility is available in Isabelle/jEdit and
+  provides a hierarchical representation of the rewriting steps
+  performed by the simplifier.  It is intended to supersede the old
+  textual tracing in a future release.
+
+  Users can configure the behaviour of the new tracing by specifying
+  breakpoints, verbosity and enabling or disabling the interactive
+  mode.  In normal verbosity (the default), only rule applications
+  matching a breakpoint will be shown to the user.  In full verbosity,
+  all rule applications will be logged.
+
+  There are two kinds of breakpoints: term and theorem breakpoints.
+  Term breakpoints are patterns which are checked for matches on the
+  redex of a rule application.  Theorem breakpoints trigger when the
+  corresponding theorem is applied in a rewrite step.
+
+  In addition to that, the interactive mode interrupts the normal flow
+  of the simplifier and defers the decision how to continue to the
+  user.
+
+  \begin{matharray}{rcl}
+    @{attribute simplifier_trace} & : & @{text attribute} \\
+    @{attribute simp_break} & : & @{text attribute} \\
+  \end{matharray}
+
+  @{rail \<open>
+    @@{attribute simplifier_trace} ('interactive')? \<newline>
+      ('mode' '=' ('full' | 'normal'))? \<newline>
+      ('depth' '=' @{syntax nat})?
+    ;
+
+    @@{attribute simp_break} (@{syntax term}*);
+  \<close>}
+
+  The @{attribute simp_break} option can be used to declare both term
+  and theorems, for example:
+*}
+
+declare conjI[simp_break]
+declare [[simp_break "?x \<and> ?y"]]
+
+text{*
+  The other options behave in a similar way as for the old trace (see
+  \secref{sec:simp-config}).
+*}
 
 subsection {* Simplification procedures \label{sec:simproc} *}
 
diff -r e0e4ac981cf1 -r 06cb5375e189 src/Doc/Isar_Ref/document/root.tex
--- a/src/Doc/Isar_Ref/document/root.tex	Mon Jul 21 14:24:10 2014 +0200
+++ b/src/Doc/Isar_Ref/document/root.tex	Mon Jul 21 15:16:50 2014 +0200
@@ -34,14 +34,15 @@
   Lucas Dixon,
   Florian Haftmann, \\
   Brian Huffman,
-  Gerwin Klein,
-  Alexander Krauss, \\
+  Lars Hupel,
+  Gerwin Klein, \\
+  Alexander Krauss,
   Ond\v{r}ej Kun\v{c}ar,
-  Andreas Lochbihler,
-  Tobias Nipkow, \\
+  Andreas Lochbihler, \\
+  Tobias Nipkow,
   Lars Noschinski,
-  David von Oheimb,
-  Larry Paulson, \\
+  David von Oheimb, \\
+  Larry Paulson,
   Sebastian Skalberg,
   Christian Sternagel
 }