[isabelle-dev] jEdit Problem report

[Makarius]

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