Hi Makarius, > * Are there remaining uses of 'file' with empty name? Is the virtual > file-system browser sufficiently convenient to inspect results > interactively?
I checked the file system browser and would be quite content with it; as a bonus you can then make use of the syntax highlighting of jEdit (OCaml seems not be built-in, though). But I want to excite more feedback of users. > * How to specify proper (unique) export names: PIDE still lacks a > check for uniqueness of export names, but overwriting existing exports > is considered illegal. The 'file' allowed to produce separate names in > the past, but it has a different meaning now (and is a candidate for > deletion). Well, if we re-consider the syntax, we will also find a way for this. > Maybe 'export_code' should be renovated replaced by reformed commands > like this: > > * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is > optional and the default something like "generated" or "code". This > could be a "thy_decl" command that updates the theory context by > generated files that are accessible in Isabelle/ML, in addition to the > export; it would also include a check for duplicate names. > > * "code_checking CONSTS in LANGUAGE" -- observing that "export_code > ... checking" is actually a different command. It would be a "diag" > command as before (this is relevant for parallelism). Maybe the »checking« should just be a variant of the regular export. Hence the modification could be quite conservative: export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME ) ( file … | ( prefix … ) ( checked ) ) where »file« denotes a relative root in the file system and »checked« indicated that the generated code will be checked implicitly. So far my current thoughts. Florian
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev