Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features
On Wed, 23 May 2012, gottfried.barrow at gmx.com 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
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