Re: [isabelle-dev] jEdit Problem report

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

[isabelle-dev] jEdit Problem report

2012-03-02 Thread Florian Haftmann 
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

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev