[isabelle-dev] jEdit import theories

[Christian Sternagel]

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