Unicode tokens: resolve font-lock issues, optimise

[David Aspinall]

Unicode tokens interacts closely with font lock but there was a problem with merging property lists for the 'face property that prevented expected behaviour with merged face attributes:

  ;; good, desirable property value for 'face 
   (append '(:slant italic) '(:weight bold font-lock-string-face))
   (:slant italic :weight bold font-lock-string-face)

   ;; bad, value obtained with font-lock-{append/prepend}-property:
   (append '(:slant italic) '((:weight bold font-lock-string-face)))
   (:slant italic (:weight bold font-lock-string-face))

for now there is a local version of font-lock-prepend-text-property with a hack to address this problem. We should discuss with Emacs developers to see how to resolve this properly. (If it is really an Emacs bug we may have to live with the ugly workaround for a while).

Additionally, some of the property mangling code could probably be optimised. The font-lock-keywords are getting quite intensive now for Isabelle!

[David Aspinall]

Another Emacs bug/issue to raise.

[coquser]

Another approach to this, probably more viable in the long run: Emacs 24.4 includes prettify-symbols-mode, which takes care of most of what we may want in terms of unicode symbols rendering. I'm not sure how it's implemented, but it feels rather snappy on my machine.

I've implemented support for this in company-coq; we could merge it.

-- cpitcla