Thinking again on this: > This optimisation becomes desirable because we have the situation with the > implementation that the control over ancestor files is fine-grained (i.e. > during scripting the file rather than at the start by parsing "imports" which > the included files behaviour assumed). I think you made this decision for > implementation ease as well as accuracy, but if you want now to > automatically retract things further than target region in certain cases, > that definitely looks like a Coq-specific function.
Actually, I realised that we do have the retraction behaviour you described for Isabelle already... If the current Coq mechanism is using proof-register-possibly-new-processed-file, we could make the retraction operation you want generic, but we'd need to implement the span based mechanism (i.e. recording the included files in the Require-like span) in the generic code too. It doesn't seem worth doing this generically because, at least for Isabelle, we had already decided to put the dependency management in the prover. Isabelle issues messages like "Proof General, you can unlock file XXX.thy" that are obeyed dumbly by PG. So the span based mechanism would conflict/overlap with that. Another way to get the behaviour for Coq might have been to implement a wrapper around coqtop that spits out these messages at appropriate points, and hope that the Coq code could be patched at some point. - D. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
