On Wed, 24 Jun 2015, Larry Paulson wrote:
This may be the problem. I don’t remember exactly what I was trying to
do, only that it was very difficult. Of course nobody uses show_types
any more. Larry
On 24 Jun 2015, at 15:13, Dmitriy Traytel <tray...@in.tum.de> wrote:
You can hover in the output panel, but you won't see types of constants
there.
Input and output of terms have always been slightly asymmetric, despite
attempts to make them agree as much as feasible over the decades.
The type annotations for certain term items in the PIDE document markup is
only half finished. It was considered impossible over many years, and
getting it to the still current state was so difficult, that I did not
revisit it again. It needs to be done one day, nonetheless.
Note that show_types is actually related to PIDE type markup: roughly
speaking, in places where show_types could work, the markup can be
provided as well.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
