clarified "simp_trace_new" and corresponding isar-ref section;
authorwenzelm
Mon, 21 Jul 2014 16:04:45 +0200
changeset 57594 8c095aef6769
parent 57593 06cb5375e189
child 57595 b73d74d0e428
clarified "simp_trace_new" and corresponding isar-ref section;
NEWS
src/Doc/Isar_Ref/Generic.thy
src/Pure/Tools/simplifier_trace.ML
--- a/NEWS	Mon Jul 21 15:16:50 2014 +0200
+++ b/NEWS	Mon Jul 21 16:04:45 2014 +0200
@@ -116,7 +116,7 @@
 "Detach" a copy where this makes sense.
 
 * New Simplifier Trace panel provides an interactive view of the
-simplification process, enabled by the "simplifier_trace" attribute
+simplification process, enabled by the "simp_trace_new" attribute
 within the context.
 
 
--- a/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 15:16:50 2014 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 16:04:45 2014 +0200
@@ -395,10 +395,12 @@
 subsection {* Simplification methods \label{sec:simp-meth} *}
 
 text {*
-  \begin{matharray}{rcl}
+  \begin{tabular}{rcll}
     @{method_def simp} & : & @{text method} \\
     @{method_def simp_all} & : & @{text method} \\
-  \end{matharray}
+    @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
+  \end{tabular}
+  \medskip
 
   @{rail \<open>
     (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
@@ -463,6 +465,9 @@
   The proof method fails if all subgoals remain unchanged after
   simplification.
 
+  \item @{attribute simp_depth_limit} limits the number of recursive
+  invocations of the Simplifier during conditional rewriting.
+
   \end{description}
 
   By default the Simplifier methods above take local assumptions fully
@@ -586,7 +591,7 @@
   apply simp
   oops
 
-text {* See also \secref{sec:simp-config} for options to enable
+text {* See also \secref{sec:simp-trace} for options to enable
   Simplifier trace mode, which often helps to diagnose problems with
   rewrite systems.
 *}
@@ -859,25 +864,32 @@
   reorientation and mutual simplification fail to apply.  *}
 
 
-subsection {* Configuration options \label{sec:simp-config} *}
+subsection {* Simplifier tracing and debugging \label{sec:simp-trace} *}
 
 text {*
   \begin{tabular}{rcll}
-    @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
     @{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\
     @{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\
     @{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\
+    @{attribute_def simp_trace_new} & : & @{text attribute} \\
+    @{attribute_def simp_break} & : & @{text attribute} \\
   \end{tabular}
   \medskip
 
-  These configurations options control further aspects of the Simplifier.
-  See also \secref{sec:config}.
+  @{rail \<open>
+    @@{attribute simp_trace_new} ('interactive')? \<newline>
+      ('mode' '=' ('full' | 'normal'))? \<newline>
+      ('depth' '=' @{syntax nat})?
+    ;
+
+    @@{attribute simp_break} (@{syntax term}*)
+  \<close>}
+
+  These attributes and configurations options control various aspects of
+  Simplifier tracing and debugging.
 
   \begin{description}
 
-  \item @{attribute simp_depth_limit} limits the number of recursive
-  invocations of the Simplifier during conditional rewriting.
-
   \item @{attribute simp_trace} makes the Simplifier output internal
   operations.  This includes rewrite steps, but also bookkeeping like
   modifications of the simpset.
@@ -890,57 +902,30 @@
   information about internal operations.  This includes any attempted
   invocation of simplification procedures.
 
+  \item @{attribute simp_trace_new} controls Simplifier tracing within
+  Isabelle/PIDE applications, notably Isabelle/jEdit \cite{isabelle-jedit}.
+  This provides a hierarchical representation of the rewriting steps
+  performed by the Simplifier.
+
+  Users can configure the behaviour 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.
+  Interactive mode interrupts the normal flow of the Simplifier and defers
+  the decision how to continue to the user via some GUI dialog.
+
+  \item @{attribute simp_break} declares term or theorem breakpoints for
+  @{attribute simp_trace_new} as described above. 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. For example:
+
   \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 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} *}
 
--- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 15:16:50 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 16:04:45 2014 +0200
@@ -419,7 +419,7 @@
   (Attrib.setup @{binding simp_break}
     (Scan.repeat Args.term_pattern >> breakpoint)
     "declaration of a simplifier breakpoint" #>
-   Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
+   Attrib.setup @{binding simp_trace_new} (Scan.lift config_parser)
     "simplifier trace configuration")
 
 end