[isabelle-dev] NEWS: Improved completion mechanism

[Makarius]

On Tue, 3 Sep 2013, Makarius wrote:

> Training my fingers a bit more, I've found that the backspace behaviour 
> makes it hard to delete keywords that can be completed.  So I am 
> considering to get rid of it again.  "Missed" completions can be 
> completed via C+b after deletion of bad parts -- I actually did not have 
> C+b when trying this at first.

See now

changeset:   53397:b179cdfa9d82
user:        wenzelm
date:        Wed Sep 04 11:12:00 2013 +0200
files:       src/Tools/jEdit/src/completion_popup.scala
description:
no completion on backspace -- too intrusive, e.g. when deleting keywords;


 	Makarius