Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features

On Wed, 23 May 2012, gottfried.barrow at wrote:

While experimenting, I saw that Linux Proof General provides certain things that jEdit doesn't. Two being that the external provers work, and that Linux PG can do searches on the Isabelle source code.

Can you explain what you mean?  What exactly does not work?

The sledgehammer suite should work smoothly in Isabelle/jEdit of Isabelle2012. It has been tested many times, and there have been many calls to report problems over several weeks.

Moreover, jEdit is particular good at searching text files, see its "hypersearch". Emacs traditionally sucks in that respect.

Having a description of all the commands like "show_types" would be useful even if the Isabelle/jEdit engine had a menu system like Proof General.

Virtually all Isabelle/Isar language elements are explained in the bulky isar-ref manual, see also

It is the most authentic and most up-to-date of Isabelle/Isar manuals.

You can see what Proof General emits on the *isabelle* process buffer, and then look up the command in the manual. This does not really work for the stateful things, though. For "show_types" you should read the general explanations about "configuration options" in the isar-ref manual, and maybe use 'print_configs' to get an idea what is available. The isar-ref manual also has a formally generated index with hyperlinks.

Note that PDF files produced by Latex cannot be searched reliably for anything outside A-Za-z0-9. So "show types" might work, but "show_types" not. Complain to Don Knuth and Leslie Lamport about not using proper ASCII by default.


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