Re: [isabelle] Isabelle/Eclipse prover IDE released!

Am 17.04.2013 00:43, schrieb Andrius Velykis:
> Dear Isabelle users,
> I am pleased to announce the first _official_ release of Isabelle/Eclipse!

Thanks for your work! Having a sane SWT-Interface alone is worth using
it (at least compared to using Swing...).

I have a couple of suggestions -- as I have never really used jEdit
(still don't like its way of user-interaction [1]), some of these might
be impossible to implement because of the underlying PIDE framework.

1.) Print some error-message if Java7 could not be found, instead of
failing silently. It took quite a while to figure this out, when the
Isabelle-View seemed to not exist.

2.) Add a view to show the 'informational' messages like "thm
list.induct". It is shown for a short moment in "prover output" but then
gone when the prover decides to proof something different. Perhaps a
view "line_number : message". This would even allow to show "term foo;
term bar" at the same time, something I really miss in PG.

2a.) As an alternative (or addition): Add a default shortcut to show the
info/error in the current line (this is the 'Show Ruler Annotation
Tooltip', as I just learned).

3.) 'export_code term in SML file -' does not produce any
output/popup/... Please add this.

4.) Sessions: If I add an external directory, how is determined, whether
there is a session?

4a.) Allow to use the logics in ~/.isabelle/Isabelle-yyyy/heaps, so that
I can use them directly without 'session dirs'.

5.) Is it somehow possible to state the logic to use via the cmdline on

So, thanks again. This really looks promising.

- René

[1] And the look'n'feel of jEdit (the editor itself) is really bad imho
-- but this is a non-technical point.

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

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