[isabelle-dev] jEdit import theories

[Makarius]

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
http://isabelle.in.tum.de/repos/isabelle/file/1ab41ea5b1c6/src/Tools/jEdit/src/jedit_thy_load.scala#l22

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.


 	Makarius