Re: [isabelle] (structure) and \<index>
On Wed, 30 Oct 2013, bnord wrote:
2. Assuming their use is still advised and appropriate for this setting:
They still seem work only using the \<bsub>..\<esub> syntax which is
broken in the JEdit interface, is there a way to move away from this?
Depends what you mean by "broken". Isabelle/jEdit still does not make any
attempt to render \<^bsub>...\<^esub> as something that looks like
subscript -- nesting would be difficult anyway. The present rendering is
not particularly pretty, but it is well-defined in what it does and what
In contrast, it has required several years to make block subscripts work
half-way in Proof General / Emacs, and there were really bad incidents on
the way. So the Emacs version is the "broken" one -- it is still possible
crash the font-lock code behind it.
When Isabelle/jEdit was started around 2008, it was unclear if subscripts
would ever work, and I was ready to give up that nice-to-have feature in
exchange for some conceptual advance in prover interaction. Later I did
find some ways to render single symbols in subscript/superscript/bold in
Isabelle/jEdit, but it required so much work that doing this again for
rarely used block-subscripts will not happen so soon.
Clemens Ballarin has already pointed out that this notation is rather
old-fashioned anyway. Which does not mean the concepts behind it are
broken, but used very rarely.
This archive was generated by a fusion of
Pipermail (Mailman edition) and