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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
