On 21.04.2012 13:20, Makarius wrote:
On Sat, 21 Apr 2012, Christian Sternagel wrote:
You should be able to use all characters in accept-characters to finish
the completion. I've just \t in there (not \n) and it works fine for me.
I removed \n, as this completes ":" to \<in> at the end of a line (like
in "lemma Foo:\n" ...
For me "\t" does not work as an accept character (nothing happens when
I type "\t"... that's the only reason why I use "\n").
I would also prefer \t, but it does nothing for me.
This seems to be a problem with Java 7 (jdk1.7.0_03); for Java 6
(jdk1.6.0_31) it works fine here (Isabelle cb44d09d9d22, JEdit build
component 20120414, Linux).
-- Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
