[isabelle-dev] Variations on show_types/show_sorts

Makarius makarius at sketis.net
Mon Oct 1 17:33:44 CEST 2012


As Florian has mentioned the topic recently on isabelle-users, I would 
like to point to Isabelle/dbadb4d03cbc: it is one more step towards live 
without changing show_types/show_sorts back and forth all the time. 
Instead, the information is already there to be uncovered by the user, 
using the usual C-hover mechanism.

This already works for type constraints and sort constraints in many 
situations, but more refinements are required to get the PIDE markup in 
the right spots.

I also need to replace the standard Java/Swing tooltip by the new 
Rich_Text_Area, such that displayed types are again subject to hovering 
and hyperlinks to get the sorts contained in some output of types, for 
example.


 	Makarius


More information about the isabelle-dev mailing list