(* Okasaki: A Web-Based Purely Functional Text Editor *)