[isabelle-dev] font issues in Isabelle jedit

[Lawrence Paulson]

The other font issue is shown below. Somehow the characters are a bit wider than jedit thinks they are, so the cursor is in the wrong place.
Larry

> On 3 Jan 2018, at 22:22, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> I seem to have fixed the problem by selecting
> 
> File > Reload with encoding > UTF-8-Isabelle

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180104/9d8a0f0b/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2018-01-04 at 18.46.30.png
Type: image/png
Size: 243707 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180104/9d8a0f0b/attachment-0002.png>