Email Gateway (Aug 22 2022 at 19:37): Email Gateway (Aug 22 2022 at 19:37):From: Dominique Unruh <unruh@ut.ee>
Hello,
in NEWS, it says
The ML function Generate_File.generate writes all generated files from a
given theory to the file-system, e.g. a temporary directory where some
external compiler is applied.
This function does not exist. I think it should say
Generated_Files.write_files.
Also, a file generated with generate_file does not show up in jEdit in
the file browser while a file generated with export_code does. (Even
though both of them show up using Generated_Files.get_files.) I don't
know if this is the expected behavior.
A small example is attached.
Best wishes,
Dominique.
Scratch.thy
Email Gateway (Aug 22 2022 at 19:37):From: Makarius <makarius@sketis.net>
This is slightly outdated, I need to revise that.
Note that the isar-ref manual has a new section "5.11 Generated files
and external files" with more detailed explanations: I've written that a
few days ago, and if you find any mistakes in proof-reading, I will
revise that as well.
Makarius
Email Gateway (Aug 22 2022 at 19:38):From: Dominique Unruh <unruh@ut.ee>
I see "5.11 External file dependencies" in the isar-ref bundled with
RC0. I assume "a few days ago" refers to a more recent version? Where do
I find that one?
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:38):From: Makarius <makarius@sketis.net>
No, it is the one I wrote for Isabelle2019-RC0.
Makarius
Email Gateway (Aug 22 2022 at 19:38):From: Makarius <makarius@sketis.net>
Err, I've got confused by the multiple branches!
The new text is after Isabelle2019-RC0, see
http://isabelle.in.tum.de/repos/isabelle/file/36821db2e356/src/Doc/Isar_Ref/Spec.thy#l1191
The same should be in the docs of
https://isabelle.sketis.net/devel/release_snapshot
Makarius
Email Gateway (Aug 22 2022 at 19:38):From: Makarius <makarius@sketis.net>
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).
Makarius
Last updated: Apr 24 2024 at 08:20 UTC