On 09/12/10 14:19, Hendrik Tews wrote:
David Aspinall<david.aspin...@ed.ac.uk>  writes:

    I think the file-load/save is a quite natural time to do this since it
    may interrupt the developer anyway and we try not to query the
    developer when sending commands in the background (so they can be
    looking at other parts of the script).

I am not so concerned any more about asking the user when sending
commands in the background. The reason is that it doesn't make
much sense to decide about recompilation on a per-file basis. I
expect that most users will either disable recompilation from
ProofGeneral or set it to "automatic" mode, where ProofGeneral
recompiles without asking back.

The "confirmation" mode, where ProofGeneral is asking for
confirmation before recompiling is probably only useful for new
users, to give them an impression about what is going on.

Did you consider the scripting time option, file activated for scripting? This is the place that saves of potential-ancestor files is triggered (with idea that prover may read them from file system). So it seems to fit this usage with caveats I mentioned before.

 - D.
ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to