Re: [isabelle] Isabelle2013-RC1 available for testing

On Thu, 24 Jan 2013, Christian Sternagel wrote:

And of course, you can change it back to your desired behavior. As follows:

1) Utilities -> Options (or C-F12)
2) Tab: Plugin Options
3) Sidekick -> General
4) "Accept characters for completion popup"
this is currently set to "\t" and you can just change it to "\t\n" (or maybe "\n")

I recommend to practice a little with \t first. In the past it just did not work for technical reasons of Java/Swing. So \n had to be used as a workaround, but it gets more often in the way of normal editing. E.g. when you type "fix x :: nat" or "foo:" and then press RETURN.

Moreover the popup passes almost all key strokes back to the main editor window, so it should get in the way much less than before.

Since the timing is also much more aggressive by default, it could break down, loosing focus or whatever. So frequent users should keep an eye on it, to see if it behaves badly. Often the problem is one of the underlying platform or the platform look-and-feel of Java/Swing. Gtk on Linux is particularly bad, because it has many themes on its own that may change the behaviour as well.

I was trying many of these things already 1-2 years ago, but it was causing so much trouble that it did not make it as default in the two earlier official releases of Isabelle/jEdit.


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