12345678910111213141516171819202122(** Escaped identifiers ["{|...|}"]. *)(** [is_escaped s] tells if [s] begins with ["{|"] and ends with ["|}"]
without overlapping. For efficiency, we just test that it starts with
['{']. *)letis_escaped:string->bool=funs->s<>""&&s.[0]='{'(** [unescape s] removes ["{|"] and ["|}"] if [s] is an escaped identifier. *)letunescape:string->string=funs->ifis_escapedsthenString.(subs2(lengths-4))elses(** [p] is assumed to be a regular identifier. If [n] is a regular identifier
too, then [add_prefix p n] is just [p ^ n]. Otherwise, it is ["{|" ^ p ^
unescape n ^ "|}"]. *)letadd_prefix:string->string->string=funpn->ifis_escapednthen"{|"^p^unescapen^"|}"elsep^n(** [s] is assumed to be a regular identifier. If [n] is a regular identifier
too, then [add_suffix n s] is just [n ^ s]. Otherwise, it is ["{" ^
unescape n ^ s ^ "|}"]. *)letadd_suffix:string->string->string=funns->ifis_escapednthen"{|"^unescapen^s^"|}"elsen^s