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
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
