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.

 - David
ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to