I used a literal "~" and changing this to "$HOME" solved the problem,
thanks!
cheers
chris
PS: Is it just me or is Isabelle/jEdit really much faster than
ProofGeneral/emacs when loading theories? (Maybe this is due to some
other difference between Isabelle2011-1 and the repo version; I only use
emacs if I have to stick to Isabelle2011-1.)
On 03/21/2012 01:24 AM, Makarius wrote:
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
