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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
