[isabelle-dev] "The following files are required to resolve theory imports"

[Makarius]

On Wed, 19 Aug 2015, Makarius wrote:

> On Wed, 19 Aug 2015, Larry Paulson wrote:
>
>>  I frequently look at finished theories when looking for useful theorems.
>>  But I’ve noticed a new and undesirable behaviour: I get the message "The
>>  following files are required to resolve theory imports” even though the
>>  theory is finished, and presumably has already been imported. Dismiss the
>>  message, and it re-appears at least once more.
>
> This is part of ongoing reforms about management of ML source files -- the 
> option is called jedit_auto_resolve, and in d94f3afd69b6 I've just changed 
> the default to give more time to rethink it.

It is back in Isabelle/46df28442a80: already loaded theories are 
suppressed.


 	Makarius