Email Gateway (Aug 18 2022 at 19:49): Email Gateway (Aug 18 2022 at 19:49):From: Alfio Martini <alfio.martini@acm.org>
Dear Users,
A simple question concerning jEdit in Isabelle. When doing the following
steps:
File -> New and typing (as an example)
theory test2
imports Main
begin
term "0 + (1::nat)"
end
and saving as test2,thy, Isabelle process successfully the input but the
output (docked) area does not update, i.e.,
for instance, when one points the mouse to right of the term expression
above. Of course this is just
a toy example to illustrate the issue in the simplest possible way.
To circumvent this problem I close and reopen the file.
This happens also when I choose (new file) in Isabelle mode.
PS: Running Isabelle 2011-1 + Ubuntu 10.04
Best!
Email Gateway (Aug 18 2022 at 19:51):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Alfio,
the same happens for me. If you have a look at "Prover Sessions" (next
to the "Output" dockable) -> "Theory Status", you will see that the new
theory is not listed. Instead of restarting jEdit you can close the file
(C+w) and open it again (C+o) (which has the advantage that other open
theory files do not have to be reloaded).
In the next release of Isabelle (which will come soon) this problem no
longer occurs.
cheers
chris
PS: the Isabelle convention is to start names of theory files with a
capital letter ;)
Last updated: May 07 2024 at 01:07 UTC