[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 MHonArc.