I like this more and more:) P. 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 > 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 >
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
