[isabelle-dev] jEdit Problem report
makarius at sketis.net
Sat Mar 3 23:28:56 CET 2012
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
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.
More information about the isabelle-dev