Utf8 notations

This replaces part 2 of #373, and is on top of #375.

This gives a file that can be imported to display unicode notations.