[isabelle-dev] jEdit import theories
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
> 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