[isabelle-dev] NEWS: refined 'help' command
Makarius
makarius at sketis.net
Tue Nov 27 16:31:33 CET 2012
* Refined 'help' command to retrieve outer syntax commands according
to name patterns (with clickable results).
This refers to Isabelle/97959912840a and Isabelle/7b73c0509835 with the
update on the isar-ref manual.
So writing "help print" somewhere in the buffer gives output with
clickable command names. The window can also be detached in the usual
way, and thus persist without its original context. This is a rather
cheap variant of "tear-off menu" by normal means of the Pretty markup
model.
Makarius
More information about the isabelle-dev
mailing list