Re: [isabelle] Jedit and export_code
On Fri, 6 Mar 2015, Lars Hupel wrote:
Just today I was thinking about that very issue, because I too find it
annoying. So here are my two cents on how I envision a proper jEdit
The command 'export_code' doesn't perform a side effect, but rather
produces a special document result containing the generated code, which
is then interpreted by jEdit. This could just be a button in the output
panel. Clicking the button opens a regular jEdit text buffer with the
generated code. In principle, the simplifier trace works in the same
Does that sound reasonable?
Yes, something like that has been in the pipeline for a long time. Maybe
I first mentioned it in winter 2012 when visiting TUM.
There are just the usual reasons why it is not done yet:
* Relatively low priority -- practical relevance is not exceedingly
* Just too many historical problems and confusions in the department of
file input or output management with the document model, in contrast
to TTY mode behaviour.
Since TTY mode no longer exists after Isabelle2014, improvements are more
likely to happen eventually.
This archive was generated by a fusion of
Pipermail (Mailman edition) and