[isabelle] Type and sort annotations in jEdit



Hi,

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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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