Email Gateway (Aug 22 2022 at 12:16): Email Gateway (Aug 22 2022 at 12:16):From: Peter Lammich <lammich@in.tum.de>
Hi list,
in the NEWS I find the following entry.
In practice this means that I have to type lots of additional <tabs>,
and set the completion tooltip delay to 0, in order to efficiently enter
symbols via \-abbreviations. Note that, in particular greek letters, are
solely accessible via their \-abbreviations.
Is there a way to get the old behaviour back, where the symbol is
completed immediately if the abbreviation is unique?
Example:
Isabelle 2015:
typing: <\> <m> <u> yields greek letter mu immediately
Isabelle 2016: Only way to get a mu that I know of:
typing: <\> <m> <u> [wait for tooltip, .5s by default] <tab>
Am I overlooking something, or is this really the default way for
entering, e.g., greek letters?
Email Gateway (Aug 22 2022 at 12:16):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
personally, I prefer the new (default) behavior. In Isabelle 2015,
whenever I wanted an alpha, my process was:
Type <\> <a> <l> <p> <h> <a>, wait for tooltip, realize I already have
"\<alpha>ha" standing there, delete the "ah".
In Isabelle 2016, there is still a problem which has been there since
Isabelle 2015:
When I want to type the comment (old), I type <(> <*> <o> and it
immediately completes to "(\<otimes>". In Isabelle 2016, I would
expect that a tooltip should ask whether to complete the "*o" to
\<otimes>.
Cornelius
Email Gateway (Aug 22 2022 at 12:16):From: Makarius <makarius@sketis.net>
On Fri, 22 Jan 2016, Peter Lammich wrote:
Is there a way to get the old behaviour back, where the symbol is
completed immediately if the abbreviation is unique?
No. "To get the old behaviour back" is one of these dangerous phrases
that provoke short answers.
There were various reasons for this simplification of completion, and
after a little bit of practice it feels very natural. It generally
reduces the surprise in different completion contexts, e.g. in document
sources with embedded antiquotations.
Example:
Isabelle 2015:
typing: <\> <m> <u> yields greek letter mu immediatelyIsabelle 2016: Only way to get a mu that I know of:
typing: <\> <m> <u> [wait for tooltip, .5s by default] <tab>
"The only way" is another dangerous phrase. For example you can use the
new etc/abbrevs facility to define your own special abbreviations.
Non-word abbrevs are immediate as before, but depend on the completion
context.
Explicit completion is unchanged: you can use C-b after a sufficiently
long prefix to complete it.
Makarius
Email Gateway (Aug 22 2022 at 12:16):From: Makarius <makarius@sketis.net>
On Fri, 22 Jan 2016, C. Diekmann wrote:
Type <\> <a> <l> <p> <h> <a>, wait for tooltip, realize I already have
"\<alpha>ha" standing there, delete the "ah".
This odd effect supported the move to the new scheme, but the key
motivation was different: allow working with Isabelle symbols in document
text, without getting insane wrt. LaTeX macros.
When I want to type the comment (old), I type <(> <*> <o> and it
immediately completes to "(\<otimes>". In Isabelle 2016, I would expect
that a tooltip should ask whether to complete the "*o" to \<otimes>.
I did not know about this odd effect, yet. It could have been discussed
long ago. We are now too close to the actual release for such
last-minutes changes -- it would require a few weeks/months of
experimentation.
I've recently seen another odd effect: .o and .O are not immediately
completed, because the dot counts as "word" letter.
I am tempted to remove all these "o" and "O" abbreviations at a later
stage, after Isabelle2016. They are not frequently used, and a bit too
irregular.
Makarius
Email Gateway (Aug 22 2022 at 12:16):From: Peter Lammich <lammich@in.tum.de>
Hi,
Note that there was an immediate completion flag, and the alpha would actually
appear after typing \alp without any waiting for tooltips or pressing of tab
or ctrl-b.
Of course, as you report, the backside was that some things where completed
too eagerly.
However, if you type a backslash in Isabelle, you almost always want a
completion. The new behaviour makes it just more typing to get it.
In my opinion, one imperfect method wad replaced by another one, but no method
is strictly better than the other. And for me, the old method workedwith less
typing overhead, that is why I want it back.
Peter
\-------- Originalnachricht --------
Email Gateway (Aug 22 2022 at 12:16):From: Makarius <makarius@sketis.net>
This is not true. Try typing some Isabelle document text, with a mixture
of Isabelle symbols and LaTeX macros. That was impossible before, and is
now quite convenient.
I have already mentioned the new etc/abbrevs a few times. It provides a
lot of freedom to invent private abbreviations. For example, you could use
"#a" = "\<alpha>" etc. You merely need to figure out a non-letter
character that is not used elsewhere in important combinations.
Makarius
Email Gateway (Aug 22 2022 at 12:16):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm used to using jedit's built-in abbreviation facility. Could you briefly explain what is different about this new one?
--lcp
Email Gateway (Aug 22 2022 at 12:17):From: Makarius <makarius@sketis.net>
On Fri, 22 Jan 2016, Lawrence Paulson wrote:
I'm used to using jedit's built-in abbreviation facility.
I am not using that myself, but it is yet another possibility for Peter to
try out. It is described in the jEdit manual.
Could you briefly explain what is different about this new one?
The default completion mechanism of Isabelle/jEdit is not really new,
merely a few policies have been fine-tuned. Thus it has become more
versatile and convenient, with less surprises.
It might require some days/weeks to get used to it, as usual.
Makarius
Email Gateway (Aug 22 2022 at 12:17):From: Makarius <makarius@sketis.net>
You can try this in $ISABELLE_HOME_USER/etc/abbrevs:
"*o" = ""
"*O" = ""
It makes these completions ambiguous, without any other effect (I think).
So there will be a popup, instead of immediate completion.
Maybe we should do this for all "o" and "O" abbrevs at a later stage.
Makarius
Email Gateway (Aug 22 2022 at 12:17):From: Peter Lammich <lammich@in.tum.de>
Ok, I never tried that with the jedit based ide.
However, the main purpose of the ide is creating Isabelle proof text, being a
convenient latex editor is a nice add on.
Although I would be much more happy with the old behaviour, I will get used to
the new one, the additional typing overhead is not that bad at all, so its
probably not worth discussing this further.
In general, whenever you do a non backward compatible change in the user
interface, you are likely to annoy some of the power users, on which you force
a new interfacing mode instead of letting them choose which they like more.
Peter
\-------- Originalnachricht --------
Email Gateway (Aug 22 2022 at 12:17):From: Makarius <makarius@sketis.net>
Even worse, accustomed power users come with clubs and pitchforks to my
doors, figuratively speaking.
Changes of Isabelle don't happen unilaterally. We usually have NEWS
announcements and possibilities for discussion on isabelle-dev months
before the public release process starts.
For Isabelle2016 that public process started 3 weeks ago. Right now we
are approximately in the middle of the hot phase, where only serious
problems are addressed.
Makarius
Email Gateway (Aug 22 2022 at 12:18):From: Makarius <makarius@sketis.net>
In Isabelle2016-RC2 I have clarifiesd that, so an empty assignment always
removes all abbreviations (independently of the order).
This is not needed, though, since all "o" and "O" abbreviations are gone.
Just too irregular and confusing for such relatively exotic symbols.
The NEWS file contains a few more words on that:
Makarius
Last updated: Apr 19 2024 at 08:19 UTC