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.

## Advertising

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