[isabelle-dev] jEdit import theories

Makarius makarius at sketis.net
Tue Mar 20 17:24:24 CET 2012

On Tue, 20 Mar 2012, Christian Sternagel wrote:

> Hi there,
> I am using an environment variable in an import statement like
> imports "$VAR/Theory.thy"
> in batch-mode this works fine. However, in jEdit I get an error message 
> indicating "Missing theory (file ...)" where the path in the error message 
> shows that $VAR was used relative to the path of the surrounding theory file. 
> $VAR contains something like "~/some-path" and was intended as being applied 
> globally.
> changeset:   e3a3f161ad70
> jedit_build: 20120313

Odd, I think it should work.  There is an explicit treatment of symbolic 
Isabelle paths (with a certain notion of variables) and the jEdit/JVM 
platform path notion.  See also

What does not work right now is to use VFS paths of jEdit together with 
Isabelle ones.  I would love to see theory sources being loaded via ssh or 
http at some point ...

In the example above, do you have a literal "~" or its expansion by the 
operating system shell?  It is more robust to use "$HOME" in shell 
scripts if you mean home.


More information about the isabelle-dev mailing list