Re: [isabelle] Type and sort annotations in jEdit



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





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