[isabelle-dev] NEWS: interactive simplifier trace
hupel at in.tum.de
Fri Mar 7 08:37:14 CET 2014
> In the Simplifier Trace panel itself I did not find out how to get
> any output. Only after pressing the "Show Trace" button a new window
> opens that contains the output.
yes, this is working as intended. The panel itself only shows
interactive questions to the user, and by default, this is switched off.
To enable it, use
> Also in the output, as opposed to [[simp_trace]] I do not see output
> for recursive calls in conditional rewriting (for the single example
> tried). Is there an option to get this?
That's another default setting: It only shows steps which triggered a
breakpoint. To override that, use
This corresponds to roughly the same content as the old trace, but with
Both settings can be combined like this:
[[simplifier_trace interactive mode=full]]
> And two general questions (sorry if this is already documented). What
> is the meaning of "Auto update" and "Auto reply" in this panel?
The semantics of "Auto update" is the same as for the output panel,
that is, if it is enabled, the contents of the panel follow the cursor
in the editing area. Disabling it thus makes the panel "attached" to the
last selected command in the editor.
"Auto reply" can be safely ignored. I don't recall exactly why I put it
there in the first place (probably for debugging reasons), so I might
remove it at some point again.
More information about the isabelle-dev