Re: [isabelle] Isabelle2013-RC2 available for testing
once more I want to bring up an older thread (back then on isabelle-dev)
about the Output Panel.
http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg03072.html
If we open a new empty theory file and do not immediately insert the
"end" (or any other character, for that matter) that belongs at the end
of a theory file, we are always one-off with the caret, i.e., error
messages as well as normal output is only visible after moving the caret
to the left once. Examples (caret position indicated by [...]):
I expect "Outer syntax error: keyword "begin" expected, but end-of-input
was found" in the Output Panel, but see nothing, if I go back to "theory
Tes[t]" the error message shows up.
theory Test imports Main begin
I expect "?t = ?t", but get nothing (again it works after changing to
find_theorems "_ = _"
It seems that the search is run, but we don't get the output until we
have "find_theorems "_ = _["]". The same hold, e.g., for sledgehammer:
the command is run, but we do not see the output.
All of this examples work as expected, as soon as at least 1 additional
character is added *after* the current position.
I think especially for beginners, starting from a completely empty file
is a common use case. End the current behavior might be a bit unexpected.
IIRC, you said that this is a general jEdit problem?
For the current release: is there a workaround (e.g., always append a
newline at the end of a new file)? Or otherwise, I would mention at a
(very) prominent place that we should always start by inserting "end" at
the end of a file. Or, even better, jEdit could insert a temple
automatically for any new *.thy file, e.g.,
where <Filename> is taken from the user (if available), <Import> might
default to "Main" and  is the initial cursor position).
[*] An aside: I would very much like to link to the "official"
isabelle-dev mail archive, but it is not searchable, and even if you
managed to find a certain message somehow, links between threads are
just cut at month borders, which makes it very hard to follow longer
On 01/29/2013 02:01 AM, Makarius wrote:
this is one more step towards the Isabelle2013 release in mid-February.
See https://bitbucket.org/isabelle_project/isabelle-release for the main
website where this is organized. There is also a link to an issue
tracker on the same Bitbucket site.
The main Isabelle2013-RC2 download page is
Observations from testing release candidates may be discussed here on
isabelle-users, on the bitbucket tracker, or via private mail.
This archive was generated by a fusion of
Pipermail (Mailman edition) and