>   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

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to