[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