On 27.06.2014 07:52, John Wickerson wrote: >> 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".) I'm pretty sure this is bound to Alt-, by default.
-- Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
