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



On Fri, 7 Jul 2006, Michael Norrish wrote:

> > 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".

So maybe ThyLoad.check_file is what you want, e.g.:

  ThyLoad.check_file NONE (Path.basic "Primes.thy");

(This example finds a file through the "$ISABELLE_HOME/src/HOL/Library"
load_path entry.)


	Makarius





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