On Fri, 2 Mar 2012, Florian Haftmann wrote:
With hg rev 07f9eda810b3: dependencies on ML files declared in theory
header are not resolved properly, e.g. try to edit
src/HOL/Import/HOL4Setup.thy
This is now addressed in 44c28a33c461.
There is a deeper conceptual mismatch behind this recurrent problem.
Theory "imports" are managed by the editor front-end, but "uses" by the
prover. To get this really right eventually, tools need to load auxiliary
files relatively to the "master" theory source, e.g. via
Thy_Load.load_file, but some details are still to be settled.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
