Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 08:33):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi people out there,

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

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

Email Gateway (Aug 19 2022 at 08:34):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 08:34):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Le Wed, 08 Aug 2012 20:27:25 +0200, Florian Haftmann
<florian.haftmann-jNDFPZUTrfRoctOpMxdO53BFZrOObVGws0AfqQuZ5sE@public.gmane.org>
a écrit:

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

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,
Florian

Yes, it did!

Email Gateway (Aug 19 2022 at 08:35):

From: Makarius <makarius@sketis.net>
The current working directory is indeed not so well-defined for GUI
applications like jEdit, especially on Windows and Mac OS. We are moving
more and more towards the "master directory" concept, i.e. files are
located relatively to the theory where you are working.

Concerning shell variables in path specifications: both Isabelle and jEdit
have their ways to integrate that. Isabelle always uses Posix notation,
extended by $VARIABLE from the environment, or the special ~ (for
$USER_HOME) and ~~ for ($ISABELLE_HOME).

jEdit does another job here: the file browser accepts platform environment
variables. So $ISABELLE_HOME will work here only for POSIX systems.
I've added an alias $ISABELLE_HOME_WINDOWS for just that, using MSDOS
notation, but that is not a real solution.

Makarius

Last updated: Apr 18 2024 at 20:16 UTC