Re: [isabelle] how do I find out which directory my theory file is in?
> On Thu, 6 Jul 2006, Michael Norrish wrote:
> Maybe this kind of peeking into theory loader internals can even be
> avoided. The theory system does not really maintain qualified
> theory names anyway. By use_thy "/foo/bar/MyTheory" or ``theory
> ... imports "/foo/bar/MyTheory"" ...'' the system merely augments
> the load path temporarily and then looks for "MyTheory.thy" as
> usual. This means when processing a thy file one may assume its
> path is already included in the lookup -- if it has been found then
> it must have been via the load path. Any subsequent load operation
> (with base file names) will go through the same procedure.
> To make a long story short, just do something like ``use
> "myfile.ML"'' to refer to auxiliary files within the same directory
> as the current thy source.
Yes. In this case, I'm loading C files with a custom piece of code,
so I need to make my code as smart as "use".
This archive was generated by a fusion of
Pipermail (Mailman edition) and