Ricardo (Oct 25 2022 at 00:53): Ricardo (Oct 25 2022 at 00:53):Hi. For quite some time I've been wanting to fill a bug in Proof General but I haven't got around it yet. The problem I have is that whenever the goals window updates, the amount of characters that fit in it horizontally is miscalculated and part of the text is left out of the window. To be able to see it I have to move the cursor to the window and then move to the area that's hidden or resize the window. Usually PG overcalculates the width by less than, say, 5 characters although sometimes I think it can be more than that. Does anyone else experience this problem? I haven't found any information on the internet yet. I think it might be related to my fonts being bigger than those of the average user but I'd think the function that performs the computation should take that into account.
Pierre Courtieu (Oct 25 2022 at 01:28):Hi. In principles pg computes the width wrt to the width of the goals buffer. I have never seen this problem except when using the text-scale feature. How do you set your fonts?
Pierre Courtieu (Oct 25 2022 at 01:29):I mean it takes the width in characters of the goal window.
Ricardo (Oct 25 2022 at 22:28):I set the font in Options -> Set Default Font... in the menu bar.
Pierre Courtieu (Oct 26 2022 at 16:31):Can you fill a bug report please? https://github.com/ProofGeneral/PG/issues
Please write the exact font you are using.
Last updated: Oct 13 2024 at 01:02 UTC