Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Isabelle2017-RC1] Superscripts not rendered i...

view this post on Zulip Email Gateway (Aug 22 2022 at 15:58):

From: Dominique Unruh <unruh@ut.ee>
Dear Makarius,

jEdit does not render superscripts correctly in my install.

See the attached screenshot from Nonnegative_Lebesque_Integration.thy
[image: Inline images 1]

(In case the screenshot gets lost: Instead of "integral" with a raised N,
it shows "integral" followed by an up-arrow, followed by "N".)

Best wishes,
Dominique.
image.png

view this post on Zulip Email Gateway (Aug 22 2022 at 15:59):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Probably the same issue, but boldface symbols do not render correctly, either.
The boldface shift character is displayed explicitly as a bold vertical bar,
rather than modifying the attributes of the subsequent character.

view this post on Zulip Email Gateway (Aug 22 2022 at 16:00):

From: Makarius <makarius@sketis.net>
This is due to the change of the plugin startup sequence, i.e. the
"Isabelle Base" vs. "Isabelle" plugins. It needs further refinement.

It should work for now if you go to Console/BeanShell and run this:

jEdit.propertiesChanged()

Makarius

Last updated: Apr 26 2024 at 01:06 UTC