Max Nowak (May 09 2021 at 19:57): Max Nowak (May 09 2021 at 19:57):I'm looking to pimp my syntax, turn things such as seq m T n into m \triangleright^{T} n, but by the looks of it whenever T is more than one character, only the first character gets printed in the super position. Is this just a limitation of Isabelle, or can I fix it somehow?
Max Nowak (May 09 2021 at 20:00):seq m TTTT n sadly is rendered as: grafik.png
Max Nowak (May 09 2021 at 20:29):Additional side issue: Defining a syntax such as _\<sub>e will render correctly, but will fail to parse when found in code. It looks like Isabelle is trying to parse all of m\<sub>e as one identifier, since doing (m)\<sub>e does seem to work. Context: Nothing hugely important, just trying to make accessors into a triple prettier (e being one of the triple elements).
Max Nowak (May 09 2021 at 20:30):I guess for now I can just do _!e instead, but that is not as neat :D
Mathias Fleury (May 10 2021 at 03:35):\<^bsup>...\<^esup> but I never remember if Isabelle/jEdit can print that....
Mathias Fleury (May 10 2021 at 03:42):After checking: Isabelle/jEdit is not able print \<^bsup>...\<^esup> correctly, but \<^bsup>...\<^esup> is how you are supposed to do it for LaTeX output
Mathias Fleury (May 10 2021 at 03:42):
Max Nowak (May 10 2021 at 09:47):That is at least a step up from what I had before, so good enough for me, thanks! :)
Last updated: Nov 13 2025 at 08:29 UTC