Re: [isabelle] Isabelle2016-RC0: cvc4 crashing



On 27/10/16 15:04, Lars Hupel wrote:
> 
>> Another issue I noticed: JEdit now forcibly resets the indentations of lines
>> with keywords such as "locale" when I type the keyword, or, what is even
>> more irritating, when I type ENTER at the end of the line.  I think this
>> new behavior is fairly disruptive of the typing habits I have established
>> to this point.
> 
> I am myself trying to get used to this, but in case you don't want the
> new behaviour, there is a way of switching it off.
> 
> Open the global options in jEdit ("Utilities" in the menu bar). In the
> left tree, pick "jEdit"/"Shortcuts". Filter for "newline". You'll find a
> command "Newline with indentation of ..." associated to "ENTER". Click
> on "ENTER" and then on "Remove Current".

I generally recommend to resist the first impulse to get back to old
habits on the spot, and first get used to new behavior, unless that
turns out to be utterly wrong.

It is part of the Isabelle development model that there is a constant
flow of changes imposed on users. This keeps both the system and the
users live and vigorous. After 30 years, Isabelle is still young and
emerging towards ultimate perfection. Just compare Isabelle98 with
Isabelle2016 for example, and compare that difference with other more
conservative systems, and than decide if you want to be back in 1998
with the established habits from that time.


More concretely on indentation: there used to be a canonical scheme
built into Proof General / Emacs over many years. When that was
superseded by Isabelle/jEdit several years ago, I did not immediately
re-implement the traditional Isar indentation for various accidental
reasons, but it was clear it would happen one day.

The current indentation scheme of Isabelle2016-1-RC0 conforms to the old
Proof General / Emacs scheme from 1998 about 98%, but there are also
additional cases, since the Isar language has changed significantly
during all these years. When implementing it, some consequences turned
out different from what I considered canonical Isar indentation over
many years -- so I also had to change a few of my old habits.

With the new default indentation always on, live has become so much
easier so that I never look back again. Suddenly there is so little to
type to get indentation right. There are still a few cases, where manual
indentation with C+i is required, but that is the opposite of the old
Isabelle/jEdit scheme to do everything manually -- and every user in a
slightly different way.

Note that the indentation of keywords performed by ENTER is meant to be
always right, while extra indentation via C+i is only a 90%
approximation: the full syntax and its delicate details are not known to
the editor (and not even to the prover).


	Makarius





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