Hi,

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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

Reply via email to