what is the rationale for overriding the user preference for
cursor-type in *goals* and *response* ?
I would expect that people who really want different cursors
within one frame, set the cursor appearance in their personal
configuration, eg via proof-shell-init-hook.
I believe setting cursor-in-non-selected-windows to nil (and
leaving cursor-type unchanged) in *goals* and *response* would be
more appropriate. This way there would be no cursor as long as
*goals* and *response* are not selected. But if the user switches
to one of these buffers in order to copy some text, then he
immediately gets his preferred cursor.
ProofGeneral-devel mailing list