I like this more and more:)
2011/1/20 Hendrik Tews <t...@os.inf.tu-dresden.de>
> David Aspinall <david.aspin...@ed.ac.uk> writes:
> Instead of what you suggested, could we add an additional
> option to p-s-ro that would give you what you want?
> I only thought about a coq-specific solution that leaves the
> other proof assistants untouched. Thinking about it, the feature
> might also be interesting for other provers.
> I would like to treat the locked material in the active scripting
> buffer and those in ancestors in different ways. I prefer the
> 'retract setting for the active buffer. However, for ancestors I
> would prefer being asked to choose one of the following:
> 1. Make scripting in ancestor ready. This is for the case that I
> want to continue with scripting in the ancestor. Proof General
> should retract up to the point where I can start scripting in
> the ancestor without being another question asked. For coq
> this means to completely retract the current active scripting
> 2. Make editing in ancestor possible. This is for the case that I
> only want to edit the ancestor and continue afterwards with
> scripting in the current active buffer. Moreover, I want to
> maintain consistency of my buffers and the prove assistant.
> For coq this means that the current scripting buffer must
> retract up to the appropriate Require command. When I change
> my mind and start scripting in the ancestor, then I am asked
> again, whether I would like to change the current scripting
> 3. Permit editing in the locked ancestor. This is for the case
> that I want to edit the ancestor without changing my current
> state in the active buffer. Thereby I accept the inconsistency
> between the buffer content and prover. For coq this means that
> only the span in the ancestor must be changed to read/write.
> When I switch to a different ancestor I want to have a new
> For coq there is usually only a tiny difference between option 1
> and 2, because Require commands are usually at the beginning of
> the file. Therefore, I would be satisfied with a choice between 2
> and 3 with the following optimisation for option 2: Proof General
> must retract at least up to the Require that caused ancestor to
> be locked. If there are only comments and Require commands above
> this point then the current scripting should be retracted
> completely. This way I can immediately start scripting in the
> ancestor. If I instead go back to the (old) active buffer,
> asserting those needlessly undone Require's is very fast.
> Alternatively a choice between 1 and 3 would be fine, if there is
> the following change for coq: If there is substantial material
> above the Require that caused ancestor to be locked, then Proof
> General should only retract up to this Require, but not the
> material before it.
> So in summary, I would like to see the following changes:
> 1. an additional option 'ask for proof-strict-read-only, which
> asks whether to retract or to permit modifications in the
> locked region.
> 2. splitting proof-strict-read-only into two variables, where one
> applies to the active buffer and the other applies to all
> other buffers.
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list