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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
