> However, I am not satisfied with what happens when I switch to > one of these looked ancestors. What currently happens is that > when I start typing there, I am forced to completely retract the > current buffer. IMO this is too much for coq.
Yes, it seems that you're actually wanting the opposite situation from Isabelle, where we suppose retracting an ancestor file is potentially expensive operation, so in general we might want to protect ancestor files against accidental retraction more enthusiastically than protecting the current script. > The situation is slightly better than I described, because one > can permit typing by setting proof-strict-read-only to nil. > However, this is a global setting which also affects the current > scripting buffer. Yes. And note that changing it is not dynamic in the sense that it does not affect spans which have been previously constructed. It is tempting to improve that in the function proof-span-read-only by always using a function (i.e. added by span-write-warning) rather than using standard read-only property. Let me understand *exactly* what you're wanting. Currently p-s-ro allows t : prevent editing without retracting manually, give read only error 'retract : automatic retraction before edits (essentially UI convenience). nil : edit freely, don't remove the span colouring or retract In nil case, the interface keeps cues about how much has been processed, but the buffer loses sync with the actual text that was processed in the sense that there is no visual indication that the text has been edited. (Remark: PGIP uses the "outdated" state I mentioned before for this condition, so an edited ancestor file would change from blue to a grey colour and cause all its children to do so also). Instead of what you suggested, could we add an additional option to p-s-ro that would give you what you want? Pro: it seems a bit smoother than your suggestion; Con: it introduces yet another user-visible choice. Something like 'edit-others, meaning nil behaviour for non-current scripting buffers. It's an easy test in the span hook function to see if we are editing in the current active scripting buffer or not. - D. _______________________________________________ ProofGeneral-devel mailing list [email protected] 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.
