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 integration:

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 way.

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 MHonArc.