Re: [isabelle] Changes in the use of the tab key
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:
^ 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and