Re: [isabelle] A trick with code generation from jEdit
On Wed, 8 Aug 2012, Yannick Duchêne (Hibou57) wrote:
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and