<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">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.<br class=""><div class="">
Larry
</div>
<div><img apple-inline="yes" id="483297C5-8DFB-4C90-B4D8-A6ECF8EC6657" width="662" height="619" src="cid:6D5F6368-9C23-4834-8729-C40C3DE69BB0" class=""><br class=""><blockquote type="cite" class=""><div class="">On 3 Jan 2018, at 22:22, Lawrence Paulson <<a href="mailto:lp15@cam.ac.uk" class="">lp15@cam.ac.uk</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html; charset=us-ascii" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">I seem to have fixed the problem by selecting<div class=""><br class=""></div><div class="">File > Reload with encoding > UTF-8-Isabelle</div></div></div></blockquote></div><br class=""></body></html>