[isabelle-dev] Extracting dependencies from theory headers

[John Matthews]

Hi Gerwin,

> On 22/12/2010, at 2:52 AM, Lars Noschinski wrote:
>> Furthermore, I would argue that current_dir should not be part of  
>> the load_path while recursively loading dependencies. The only time  
>> current_dir should be considered is when loading a theory file  
>> "from the toplevel
>
> Seconded. This causes quite a bit of confusion every time new users  
> come in.

I'm not quite sure what "recursive dependencies" means here. However I  
think it's important to support the use-case where a new-ish user  
decides to split their single theory into two or more separate  
theories in the same directory and have one theory import the others.  
Would this still be supported?

-john
  
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2205 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101221/f1b42de1/attachment.bin>