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

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").


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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