[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