> 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.
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.