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:

  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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.