Re: [isabelle] Isabelle2013-1-RC4 available for testing



On Mon, 11 Nov 2013, Andreas Lochbihler wrote:

I also experienced that popups swallow characters, and it happens with all characters, not just underscores. For me, it most likely happens when Isabelle works a lot in the background. My system parameters: standard 12.04 LTS Ubuntu Linux.

I've made some re-adjustements after the Isabelle2013-1-RC4 snapshot: see https://bitbucket.org/isabelle_project/isabelle-release version 9c1f21365326. Can you give it a quick try? You know how to work with repository versions.


The documentation for the change is like this:

  \item The system option @{system_option
  jedit_completion_dismiss_delay} determines an additional delay (0.0
  by default), before dismissing an earlier completion popup.  A value
  like 0.1 is occasionally useful to reduce the chance of loosing key
  strokes when the speed of typing exceeds that of repainting GUI
  components.

My impression is that Linux users who type very quickly are apt to see the problem with some probability. On Windows, the Java GUI performance is much better, but I've seen the same when running a remote Windows session over a slow connection.


The next time I pass by the completion mechanisms, I will remove any attempts to do a GUI focus change. After studying the AWT/Swing documentation and sources quite some time, I came to the conclusion that this is inherently difficult to get right, despite some explicit mechanisms to queue/dequeue "typeahead key events" in the AWT event handler.

What I actually wanted to do last summer was to provide context-sensitive completion, based on information provided by the prover. Then I got stuck with many such GUI issues, and these timing problems are just the last bits of it.


	Makarius




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