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



On Thu, 6 Jul 2006, Michael Norrish wrote:

> I am implementing an Isar toplevel directive that takes a filename as an 
> argument.  I'd like to interpret this as relative to the directory 
> containing the enclosing theory file

First of all note that actual theory values have no notion of the source 
text or file-system location.  You may still get something like this by 
asking the theory loader, e.g. using Context.theory_name and 
ThyInfo.loaded_files.  The latter merely records file dependencies, but 
the main thy source will show up as head element eventually.  (The file 
list may well be empty, e.g. in interactive composition of theory sources 
without loading any files.)

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.


	Makarius





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