Hi, 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. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
