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 not.

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 MHonArc.