[isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 01/02/2019 15:30, Lars Hupel wrote:
> 
>>   * no generated files in the repository (these are not sources but
>> results from sources)
> 
> What about generated theory files? This also affects the CakeML entry. I
> could easily package Lem as a component, but how would "isabelle build"
> call it?

The present reform is mainly about generated output files, not input
theory files.


The standard approach for the latter is to have the other tool directly
import its source format into the theory context within Isabelle/ML,
without the intermediate theory source. Doing this carefully, would even
produce nice PIDE markup for the original sources. PIDE is an IDE for
arbitrary user-defined languages.

It might be worth doing this for tools like Lem eventually, but I have
not looked at it closely so far.


	Makarius