Great list Peter! > * The standard search (Ctrl-F) function does not allow to enter > non-ASCII characters at all. This is a real show-stopper if you search > for a text containing such characters. In PG, you could at least use > \<...> - tokens to enter non-ASCII characters. > > Moreover, I would like an incremental search, but there is probably a > jEdit pluging somewhere? (Probably with the same problems of entering > non-ASCII characters)
There is already an incremental search, but by default it has no keyboard shortcut. Myself, I have re-bound Ctrl-F to "Incremental Search Bar", and am quite happy with that. (This is in jEdit's "Global Options", then "Shortcuts".) John _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
