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