[isabelle-dev] jEdit import theories
c-sterna at jaist.ac.jp
Wed Mar 21 08:18:22 CET 2012
I used a literal "~" and changing this to "$HOME" solved the problem,
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
> 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