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
