Hendrik Tews <t...@os.inf.tu-dresden.de> writes: 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.
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. >From my understanding of Proof General, the read only behaviour of the locked region is achieved by the span in proof-locked-span. If this is right, I would suggest to change the 'modification-hooks and 'insert-in-front-hooks of the span proof-locked-span for coq for all buffers except the current scripting buffer. To achieve this I would setup appropriate functions in proof-activate-scripting-hook and proof-deactivate-scripting-hook. For the initialisation of the proof-locked-span I would change the call of (proof-span-read-only proof-locked-span) in proof-init-segmentation (funcall proof-initialise-proof-locked-span-read-only) where (proof-span-read-only proof-locked-span) is the default value of proof-initialise-proof-locked-span-read-only. Coq mode would of course overwrite proof-initialise-proof-locked-span-read-only. Comments? Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
