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

[Makarius]

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.

The reason why it came up right now is the new ML debugger IDE (which 
requires a recent repository version of Poly/ML).  Once that is stablized, 
I will announce it here for public exposure and more serious testing.  It 
has the potential to change the way we work with Isabelle/ML development 
fundamentally.


 	Makarius