Re: [isabelle] Isabelle2013-RC2 available for testing



Dear Makarius,

once more I want to bring up an older thread (back then on isabelle-dev) about the Output Panel.

See 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 [...]):

  theory Test[]

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
  thm refl[]

I expect "?t = ?t", but get nothing (again it works after changing to "thm ref[l]").

  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.,

  theory <Filename>
  imports <Import>
  begin
  []
  end

where <Filename> is taken from the user (if available), <Import> might default to "Main" and [] is the initial cursor position).

cheers

chris

[*] 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 threads.)

On 01/29/2013 02:01 AM, Makarius wrote:
Dear all,

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
http://isabelle.in.tum.de/website-Isabelle2013-RC2

Observations from testing release candidates may be discussed here on
isabelle-users, on the bitbucket tracker, or via private mail.


     Makarius







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