[isabelle] Changes in the use of the tab key
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).
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875
This archive was generated by a fusion of
Pipermail (Mailman edition) and