Email Gateway (Aug 19 2022 at 15:58): Email Gateway (Aug 19 2022 at 15:58):From: Joachim Breitner <breitner@kit.edu>
Hi,
I’m not sure if this is an issue with jEdit or with Isabelle/jEdit, but
I find the default number of 100 undo steps very low, and I occasionally
lose work when some change turned out to be contraproductive and I want
to go back.
Given the resource demands that Isabelle has anyways (16GB RAM was
suggested recently, I think), I don’t believe that there is a problem
raising that limit by an order of magnitude or two.
I know I can change it myself locally, but
when upgrading Isabelle my settings are lost, so unless I’m very
careful I’ll be bitten by the problem at least once per release.
other users might learn about the setting the hard way.
So I suggest to change the default as distributed with Isabelle.
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:58):From: bnord <bnord01@gmail.com>
I wouldn't recommend using jEdit undo at all, you can't undo undos (as
in emacs) so you live with the illusion you can get back to previous
states while a single edit after an undo can cut of arbitrary parts of
your documents history.
Email Gateway (Aug 19 2022 at 15:58):From: Makarius <makarius@sketis.net>
On Tue, 30 Sep 2014, Joachim Breitner wrote:
I’m not sure if this is an issue with jEdit or with Isabelle/jEdit, but
I find the default number of 100 undo steps very low, and I occasionally
lose work when some change turned out to be contraproductive and I want
to go back.
I have never encountered this limit myself in 8 years of using jEdit as my
main editor, as well as a few years of using Isabelle/jEdit as Prover IDE.
After spending 5min with the sources and properties of jEdit, I now see
that there is buffer.undoCount, which can be changed in Global Options /
Editing / Number of undos. The change is made persistent in
$ISABELLE_HOME_USER/jedit/properties as usual.
It is normal that personal properties accumulate, and require manual
maintenance on Isabelle releases. The main inconvenience here is the
erratic order of the lines in the file -- something that is worth
improving and submitting to one of the trackers at
http://sourceforge.net/projects/jedit
I could add more Isabelle/jEdit default changes to
$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props, but it needs a minimum
level of significance to diverge further from the defaults.
Given the resource demands that Isabelle has anyways (16GB RAM was
suggested recently, I think)
There is a misunderstanding: Isabelle/jEdit resource requirements are not
very special. A small machine for small applications (4 GB RAM), a medium
machine for medium applications (8 GB RAM), a slightly bigger machine for
big applications (16 GB). Really big machines by today's standards have
32-128 GB RAM.
That may sound hilarious, but Proof General with XEmacs required much more
resources in relation to the hardware of its time. When crafting
Isabelle/jEdit over so many years, I always kept an eye on current
consumer hardware parameters. One problem that I did not foresee is the
general stagnation of the market: people don't upgrade their machines
anymore as they used to do in the past.
I don’t believe that there is a problem raising that limit by an order
of magnitude or two.
I don't know much about the jEdit undo manager, so I can't tell. This
discussion is better moved to
http://sourceforge.net/p/jedit/mailman/jedit-devel
So far I have been mostly alone on that mailing list to represent the
needs of Isabelle/jEdit users.
I need to emphasize once more that Isabelle/jEdit is not a fork of jEdit,
but an application on top of it. As much required changes as possible
should be handed back to the main project, even though this is some extra
work.
Makarius
Email Gateway (Aug 19 2022 at 15:59):From: Makarius <makarius@sketis.net>
Using Emacs myself over 15 years, I never understood its way of undo or
undo-undo.
jEdit is more standard in that sense: it follows customs from the
1980/1990-ies that are well-established in many applications. There is
undo and redo to move in the history in the normal way. There might be
questions how the graniularity of history steps is actually determined,
but that is something for regular jEdit user channels. Myself I just
adopted the mechanics of the existing editor in my editing -- as I did for
other editors in the past.
How about someone opnening a question on stackoverflow with tag "jedit"
(not "isabelle")? Or posting on some jedit mailing list?
Makarius
Email Gateway (Aug 19 2022 at 15:59):From: bnord <bnord01@gmail.com>
jEdit:
A -edit-> B -edit-> C -undo-> B -edit-> D -undo-> B (*) -undo-> A
(*) no way to get back to C from here
emacs:
A -edit-> B -edit-> C -undo-> B -edit-> D -undo-> B -undo-> C -undo-> B
-undo-> ...
There is an edit stack with an undo pointer, each edit command sets the
undo pointer to the latest element except the undo command which is an
edit command that decrements the undo pointer and reverts the command
pointed to by the undo pointer.
Email Gateway (Aug 19 2022 at 15:59):From: Makarius <makarius@sketis.net>
I still don't quite understand the point. Is this now something for the
mailing list of jEdit or Emacs?
Isabelle/jEdit is the second major prover front-end, after Proof General
Emacs, where I was also involved. The editor substrate at the bottom is
given as-is. It has strengths and weaknesses. As an editor I've found
jEdit more onvincing than Emacs, which is why I started this insane PIDE
project, but PIDE is actually independent of editors.
There are two main routes to go from here:
* participate in improvements of jEdit on the jEdit mailing lists,
trackers etc.
* participate in other PIDE implementations, e.g. Isabelle/Eclipse.
Makarius
Last updated: Apr 20 2024 at 08:16 UTC