[isabelle] Isabelle2019-RC0: generate_file - documentation and behavior

On 09/04/2019 10:53, Dominique Unruh wrote:
> The documentation matches what I expected.
> I am still confused about the behavior of the jEdit file system browser
> in combination with those commands.
> I did not find documentation for the file system browser, but my
> understanding is that under "isabelle-export:" I find all exported files.

That documentation is still missing: it will be in an updated "jedit"
manual later in the release process.

> As you see from the output panel, two files are generated according to
> Generated_Files.get_files (this is what I would expect).
> But only the file generated via export_code shows up in the file system
> browser.
> Is that intentional? From the documentation in isar-ref, my
> understanding is that both command just generate virtual files (the only
> difference being how the content is generated).

There are two different concepts: "generated files" within the theory
context of Isabelle/ML, and "exported files" within the session context
of Isabelle/Scala (the latter has some explanations in the "system" manual).

The isabelle-export: VFS in jEdit only sees exported files, not
generated files.

There are easy ways to export generated files, e.g. the
'export_generated_files' command.

The 'export_code' command does both by default, thus you see the result
in the browser.

Also note that the browser needs to be manually updated via the reload
button, whenever there is a change in the content. Thus it is not fully
PIDE conformant (similar to Sidekick).


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