>> It seems there is a little (but annoying) issue with the new tooltips in >> Isabelle/jEdit when using a font other than IsabelleText. I'm using the >> Source Code Pro font and the tooltips are always just a little too small so >> that part of the text is hidden/cut off. Of course an easy fix would be to >> go back to using IsabelleText... > > Did you try this again? > > Last week I've refined it a little bit, in the vicinity of > Isabelle/4f2b5b2a9ad5. It is a bit better, but not really precise, just some > heuristics that I've tried with the 5 most common fonts that I know of, and a > range of font sizes. (I am still not convinced of Source Code Pro at all, > despite its name and the marketing they made some weeks ago.)
I just tried it, and it now works perfectly with Source Code Pro. Awesome, thanks! Steffen _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
