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.


	Makarius


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