Re: [isabelle] A trick with code generation from jEdit

Hi Yannick,

> Writing
>   export_code f1 f2 … in SML file "filename"
> is tricky from jEdit. As evaluation occurs as you edit, you get multiple
> files generated in your home directory, as you enter "filename"
> character by character. Ex. you will get one file named "f" then another
> named "filen" then finally another named "filename", all with the same
> content (obviously).

this, indeed is annoying, but at the moment there is no proper concept
for »Isar commands with side effect« in Isabelle/jEdit.  As a
workaround, I suggest to write something like

  export_code … in SML "filename"

in the first instance and then insert the »file« later (this is,
admittedly, a little bit silly).

> By the way, how do you change the default output directory? Do you have
> to always provide an absolute full path?

Currently, the output directory is relative to the current working
directory.  In future Isabelle releases, it will be the master path of
the theory.  There is no default output directory apart from that.  Note
that you can use environment variables $FOO in path specifications if
there is need to organize predefined locations in the file system.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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