Re: [isabelle] Isabelle2013-RC2 available for testing

On Wed, 30 Jan 2013, Christian Sternagel wrote:

If we open a new empty theory file and do not immediately insert the "end"

So why do it without? You need the end eventually, so you can make it part of the standard habit of starting a new theory.

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.

IIRC, you said that this is a general jEdit problem?

Yes, jEdit has a blind spot at the very end of the buffer, due to special tricks it does for handling files with or without final line terminator. Even worse, the numeric length of the buffer is one off, so plugins unaware of that easily produce NPE particles. I have once tried to file a tracker item at the jEdit project, but these guys are not as reactive as we are here on the Isabelle mailing lists. One should try again, ideally in a constructive version, i.e. a patch proposal for jEdit.

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.

I think genuine beginners don't even get that far. They need to be told to open some .thy file and put a certain template there. Some people do not even manage to get Isabelle/jEdit start up -- in the last two releases I tried to improve the success rate at that spot primarily.

For the current release: is there a workaround (e.g., always append a newline at the end of a new file)?

The Isabelle2013 codebase already has various internal workarounds, and it is close to a local optimum that is hard to change without breaking things again. There used to be funny effects when moving the caret, like showing old versions of output, instead of showing nothing, as it should be now.

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

Most people don't even read the most prominent bits of information, like ANNOUNCE or NEWS. It is better to make jEdit put a template there without too much hassle, but that old idea did not make it in the Isabelle2013 release.

What could be done right now is to make a nice video for the first encounter with Isabelle/jEdit, and put this somewhere on youtube.

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

I never know myself how to quote our mailing lists and just use an arbitrary archive from the main Isabelle website.


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