I'm not sure if the reason for the cursor change was explained: the
hollow box indicating cursor position was sometimes causing confusion
with mathematical notation appearing in the output (e.g. box operator).
> I believe setting cursor-in-non-selected-windows to nil (and
> leaving cursor-type unchanged) in *goals* and *response* would be
> more appropriate.
I agree, especially since its effect is local. Not sure why the other
setting was chosen originally.
Thanks for the improvement.
I've pushed another pre-release just now.
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.