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