[isabelle-dev] »real« considered harmful

[Makarius]

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 <traytel at 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