coq2html does not like Unicode

coq2html gets confused when unicode characters are used in identifiers. Here is a small example

Inductive ωtruth :=
| ωtrue : ωtruth
| ωfalse : ωtruth
| otrue : ωtruth
| ofalse : ωtruth.
Definition otruth := ωtruth.

Reserved Notation  "'¬' t" (at level 50).
Definition ωneg (ω:ωtruth) : ωtruth :=
  match ω with
  | ωtrue => ωfalse
  | ωfalse => ωtrue
  | otrue => ofalse
  | ofalse => otrue
  end.
Notation  "'¬' x" := (ωneg x).
Definition oneg := ωneg.

Lemma ωdoubleneg :
  forall (ω:ωtruth), ¬(¬ω) = ω.
Proof.
  destruct ω; reflexivity.
Qed.

Lemma odoubleneg :
  forall (o:otruth), oneg (oneg o) = o.
Proof.
  destruct o; reflexivity.
Qed.

The o-prefixed identifiers are handled properly but not the ω-prefixed ones.

I'm afraid no attention to Unicode was paid so far in the implementation of coq2html! Indeed, the regexp for identifiers

coq2html/coq2html.mll

Line 274 in d68b757

let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']*

is ASCII-only. I need to look at how Coq itself handles Unicode in identifiers.

I don't recall how ocamllex does with unicode. I had a very good experience with Alain Frish's sedlex https://github.com/alainfrisch/sedlex

ocamllex doesn't know anything about Unicode but it might be able to do something with the UTF-8 encoding of Unicode. I, too, was thinking of ulex and its successor sedlex.