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 buffer. 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 buffer. 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 choice. 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. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
