[isabelle-dev] NEWS: interactive simplifier trace

[Lars Hupel]

 Hi Chris,

> 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

   [[simplifier_trace interactive]]

> Also in the output, as opposed to [[simp_trace]] I do not see output
> for recursive calls in conditional rewriting (for the single example 
> I
> 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

   [[simplifier_trace mode=full]]

 This corresponds to roughly the same content as the old trace, but with 
 hierarchical structure.

 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.

 Cheers
 Lars