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

Am 17.04.2013 19:28, schrieb Andrius Velykis:
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.

Do you mean like a duplicate Prover Output view that is "sticky" on some
prover command?

Yes. Perhaps exactly those commands, that already produce the (i)-bubble to the left of the text.

Could you file this as an issue and elaborate more in (you can use the tracker to record feature requests as well as bugs!)? I am not too familiar with PG (never got used to Emacs..) so would appreciate more details :)

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

Could file an issue and elaborate further? Thanks!

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

The session dir must have an appropriate ROOT or ROOTs file at the top (see
Chapter 3 in Isabelle System Manual).

Ah, will look into it. Never had to use this -- having a ROOT.ML and a ./ did the thing for me until now.

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

You can build sessions into your home directory by selecting "Build
sessions to user home directory" in Build tab of Isabelle launch
configuration. Or do you mean that the dialog should look for additional
heaps already pre-built there and list them in the session selection?

The latter. Because then, my current setup (ROOT.ML + would still work, and I wouldn't need any session directories.

I am
not sure how much Isabelle.Build tool covers this (Isabelle/Eclipse just
provides a UI for it).

Well ... there still is `isabelle findlogics`. But I don't know, how this is implemented.

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

No, not at the moment. It is not possible to auto-start Isabelle, you have to start it manually via the configured launch dialog. In Isabelle/Eclipse
I am still investigating the best way of interacting with Isabelle
distribution, since it is not bundled with a specific Isabelle like
Isabelle/jEdit (see

What is your use case to indicate the logic via cmdline?

With some project-oriented environment like Eclipse, there probably is none. For PG I used to have ".isabelle-logic" files all over the place, which specify the logic image to use, and then a wrapper around 'isabelle {emacs,jedit}' that interprets them (cf. ). So the question was more or less inspired by current habits :).

- René

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

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