Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Escaped identifiers "{|...|}"
.
is_escaped s
tells if s
begins with "{|"
and ends with "|}"
without overlapping. For efficiency, we just test that it starts with '{'
.
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 ^ "|}"
.