Re: [isabelle] Isabelle2013-RC1 available for testing



On 23.01.2013 15:09, Slawomir Kolodynski wrote:
The hints in jedit are less convenient  in Isabelle2013, I don't know if this is intentional. For example, if I type \<ta I get the only hint for the greek letter \<tau>.
It used to be that if I pressed enter at this point it was interpreted as selection and the text \<ta was replaced by the full text \<tau>in the source. Now jedit just puts the cursor in the new line. To select \<tau>  I have to point and click the mouse.
Similarly, if I type \<in I get a couple of possibilities. If I point the cursor (with arrows on the keyboard) to the symbol \<in>  and press enter, again this just puts me in the new line instead of selecting \<in>. I would prefer not to have to switch between keyboard and mouse every time I want to select a symbol from the hints. Can it be configured in options somehow?

As far as I know, the completion key was changed from \n (Enter) to \t (Tab).

  -- Lars





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