Email Gateway (Aug 19 2022 at 17:03): Email Gateway (Aug 19 2022 at 17:03):From: "W. Douglas Maurer" <maurer@gwu.edu>
Before Isabelle2014 came out, I put together a write-up for my
students, based on Isabelle2013, which, among other things, covered
entering special characters using the tab key. For example, you could
enter <= followed by the tab key and the single less-than-or-equal
character would come up on the screen. In Isabelle2014, this is
improved; you just type <= without the tab key and the single
character comes up. That is helpful, and I will change my write-up to
reflect that. (In particular, this is faster than finding the proper
button in the Symbols panel and clicking that.)
However, I now find that some of the other uses of the tab key don't
work any more. In particular, I used to be able to type colon-tab to
get the is-a-member-of character, and that doesn't work in
Isabelle2014. If I hover over the button for that character in the
Symbols panel, the only abbreviation that shows there is the colon
character. I could still type \<in>, but doing that would not be
faster than finding the button for is-a-member-of and clicking on it.
The same problem arises for other characters, such as ! tab to get
the forall character, and ? tab to get the exists character. I can
still use ALL tab to get the forall character, but EX tab (for the
exists character) doesn't work.
Another problem (for which there is a workaround) would arise if I
wanted to enter the string "<=" . If I enter this directly, the <=
automatically converts to the single less-than-or-equal character.
The workaround is to type "=" and then go back and insert the <
character before it. That does work, but it's clumsy.
Other systems that I have used employ a convention here, involving
the backspace (or delete) character. For example, when I type a row
of asterisks on my word processing program, and then hit return, the
asterisks convert to a row of small black squares. This looks nice,
but, if I don't want this, I can immediately hit backspace, and the
row of asterisks will reappear. I would like to be able to do this
with <= (so I would type <= backspace and it would give me the two
characters < and = whether inside quotes or not).
Email Gateway (Aug 19 2022 at 17:10):From: Makarius <makarius@sketis.net>
On Wed, 4 Feb 2015, W. Douglas Maurer wrote:
Before Isabelle2014 came out, I put together a write-up for my students,
based on Isabelle2013, which, among other things, covered entering
special characters using the tab key.
If you want you can show me the write-up, so that I see what kind of
really important information needs to be given in the Isabelle/jEdit
manual.
For example, you could enter <= followed by the tab key and the single
less-than-or-equal character would come up on the screen. In
Isabelle2014, this is improved ...
Did you see the extended section "3.5 Completion" of the Isabelle/jEdit
manual?
If there is anything missing or unclear in the text, I am ready to listen.
If there is anything missing or unclear in the concepts and their
implementation, particular points might get queued in the pipeline (the
metaphorical one one that leads from Central Asia to Europe).
Makarius
Email Gateway (Aug 19 2022 at 17:15):From: Makarius <makarius@sketis.net>
On Wed, 4 Feb 2015, W. Douglas Maurer wrote:
However, I now find that some of the other uses of the tab key don't
work any more. In particular, I used to be able to type colon-tab to get
the is-a-member-of character, and that doesn't work in Isabelle2014. If
I hover over the button for that character in the Symbols panel, the
only abbreviation that shows there is the colon character. I could still
type \<in>, but doing that would not be faster than finding the button
for is-a-member-of and clicking on it.
(Back to the original question, without any meta-questions and diverging
private threads on other topics.)
I guess that above you merely experience the effect of the semantic
context of completion in Isabelle2014. It should work as expected, if you type
into a term context, e.g. via the Isar command 'term' like this:
term ""
^ now type text here, after waiting a bit
The same problem arises for other characters, such as ! tab to get the forall
character, and ? tab to get the exists character. I can still use ALL tab to
get the forall character, but EX tab (for the exists character) doesn't work.
That is the same situation.
Another problem (for which there is a workaround) would arise if I wanted to
enter the string "<=" . If I enter this directly, the <= automatically
converts to the single less-than-or-equal character. The workaround is to
type "=" and then go back and insert the < character before it. That does
work, but it's clumsy.
You can use "undo" of the editor to undo the completion, as explained in
the "jedit" manual.
Makarius
Last updated: Apr 25 2024 at 12:23 UTC