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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
