> 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.
Maybe -- but I prefer to avoid proliferating user options even further unless there's a desire (ideally from more than one user...). Also, we should avoid making the code overly complicated (and the automatic functionality difficult to guess) if the use case you are addressing could be managed just by the user very easily hitting another key press (e.g. C-c C-r) that becomes part of their work flow. I had in mind us adding one additional option for p-s-ro, not turning it from three settings into 8, so let's think about it... > 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. OK, so this is current 'retract setting, right? > 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. If I understand right, I think the main new use case you're allowing here is for the user to make an edit in an ancestor file, and have that file automatically recompiled (not scripted) by re-processing the Require line in the child buffer and without nuisance of having switched active scripting buffer, etc. Before making that an automatic option for p-s-ro it could be implemented as a user-level command perhaps, and if you want the precise (retract to line of Require) behaviour, for Coq only. > 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. Hmm. This sounds like something for consenting adults only, and something that C-c C-z, proof-frob-locked-end should allow. Have you used that command? > 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 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. > 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. Yes, I agree for Coq. Although I notice again it's just one key/button press for the user, C-c C-r. > 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. This seems to be an additional dialogue that's not really necessary (the user can manually retract with C-c C-RET when p-s-ro is strict). Perhaps you mean to change the buffer local behaviour temporarily for just the current buffer. Would a buffer-local override to allow edits temporarily meet this? (alternative to C-c C-z, edit, C-c C-z) > 2. splitting proof-strict-read-only into two variables, where one > applies to the active buffer and the other applies to all > other buffers. Not sure about this, and it might be messy in the code. Easier would be a buffer local value for proof-strict-read-only which can be modified from the default, but I'm not sure how smoothly that would work in the code, and it is tricky to explain that in the UI --- this is why several of the current menu commands make extra work for themselves to modify a setting across all scripting buffers uniformly (e.g., tokens, read only, ..). - 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.
