Re: [isabelle] jEdit (unexpected?) behavior



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 ;)

On 05/02/2012 12:45 PM, Alfio Martini wrote:
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!






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