On Wed, 21 May 2014, Makarius wrote:
Concerning the missing German dictionary: it is easy to include additional
dictionaries as plain word lists. Users can do that via JORTHO_DICTIONARIES
in the settings environment.
Actually, I have forgotten an important detail: German uses capitalization
in a manner that is absent in English. JOrtho is by some German guy, and
he had many adhoc flags for that, but I simply by-passed that complication
to make it work smoothly for English.
So at the moment it would probably work for French, but not for German.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
