[isabelle] Type and sort annotations in jEdit

[Florian Haftmann]

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

[Makarius]

On Sat, 22 Sep 2012, Florian Haftmann wrote:

> Currently, in jEdit one can do something like
>
> setup {* Config.put_global Printer.show_sorts true *}
>
> similar to what one has done in PG.

Since this option is embedded into the Isar attribute space, you can
use this equivalent form:

declare [[show_types]]

> 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?

Just last week I've started revisiting these ideas. The next release will
have output with hyperlinks and tooltips, as you see them in Isabelle2012
for the input source already.

It is just a matter to modify output produced by the prover to annotate
constraints (types for term variables, sorts for type variables) using the
existing infrastructure of PIDE document markup. This requires some
care, though, since the total type information is an order of magnitude
larger than then the term information without constraints.

Just a few days ago, I've managed to make the new Isabelle/jEdit "rich
text area" fit for huge term collections produced by 'print_theory' or
'find_theorems (9999) _' such that > 0.25 MB is rendered in < 0.5s without
blocking the GUI. Exercising this sport a bit more, there is some hope
that for the next release full types/sorts can be included by default.

The user may then inspect hyperlinks or tooltips hierarchically to reveal
more and more of the information that is implicit in the document model.


Makarius

[Makarius]

On Sat, 22 Sep 2012, Makarius wrote:

> On Sat, 22 Sep 2012, Florian Haftmann wrote:
>
>> Currently, in jEdit one can do something like
>>
>> setup {* Config.put_global Printer.show_sorts true *}
>>
>> similar to what one has done in PG.
>
> Since this option is embedded into the Isar attribute space, you can
> use this equivalent form:
>
> declare [[show_types]]

This should be "declare [[show_sorts]]". Both can be handled somewhat
uniformly, despite some slight differences in the internal concepts.


Makarius