Re: [isabelle] how do I find out which directory my theory file is in?



Makarius writes:
> 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".

Michael.

 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.