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

Le Wed, 08 Aug 2012 20:27:25 +0200, Florian Haftmann <florian.haftmann-jNDFPZUTrfRoctOpMxdO53BFZrOObVGws0AfqQuZ5sE at> a écrit:

Hi Yannick,


  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).

Seems strange indeed, but not that much blocking anyway. Was to drop a note in case no body noticed.

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.

OK, I didn't know shell variables was allowed there. After you said the output directory it the current directory, I've just updated the launcher which opens*.thy file, so that it switch to the theory file's directory prior to the invocation of “isabelle jedit "$1"” (cd `dirname "$1"` in a wrapper script, if your environment have bash). That do the thing, as output in the theory directory (or a subfolder of), is what one probably expect.

Hope this helps,

Yes, it did!

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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