Re: [isabelle] Feature suggestion: Replace statement by pretty-printed statement



Although I do not do this editing that Joachim describes, I also sometimes
wish that defnitions and lemmas would print the proposition to see what it
looks like.

Tobias

On 30/04/2014 11:16, Joachim Breitner wrote:
> Dear List,
> 
> I am currently doing something tedious that I find myself doing often: 
> After having finished a theory I polish it up, including adding nicely 
> looking notation. And then I begin going through my theory, putting the 
> cursor on any lemma declaration or "have" and copy the nicely printed 
> output from the output buffer to the editor buffer.
> 
> For definitions and "assumes", I first have to call "thm foo_def" or "thm
> assms" to get hold of that display.
> 
> It would be great if that process was made easier, maybe by a button in the
> popup that is (sometimes?) visible when I hover over such a statement, or
> even better a keyboard combination (similar to how jEdit will format a
> paragraph when I use "C-e f").
> 
> 
> Thanks, Joachim
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.