Re: [isabelle] Type and sort annotations in jEdit



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.