[isabelle] Type and sort annotations in jEdit


in certain situations in is necessary to inspect sort constraints of
type variables and similar things in theorems and proof states.

Currently, in jEdit one can do something like

  setup {* Config.put_global Printer.show_sorts true *}

similar to what one has done in PG.

What seems more desirable is that mouseover-tooltips for type variables
would carry sort constraints (similar for term variables / constants and
type constraints).  Is there already something to configure Isabelle
that way, or, in a broader perspective, what are the currently floating
ideas how inspection of sort constraints should be accomplished in jEdit?

Thanks a lot,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.