+
+// Escape '<' and '>' and remove richtext markers (e.g. {!this is richtext!}) from a string.
+docstring processRichtext(docstring const & str, bool richtext)
+{
+ docstring val = str;
+ docstring ret;
+
+ bool scanning_rich = false;
+ while (!val.empty()) {
+ char_type const ch = val[0];
+ if (ch == '{' && val.size() > 1 && val[1] == '!') {
+ // beginning of rich text
+ scanning_rich = true;
+ val = val.substr(2);
+ continue;
+ }
+ if (scanning_rich && ch == '!' && val.size() > 1 && val[1] == '}') {
+ // end of rich text
+ scanning_rich = false;
+ val = val.substr(2);
+ continue;
+ }
+ if (richtext) {
+ if (scanning_rich)
+ ret += ch;
+ else {
+ // we need to escape '<' and '>'
+ if (ch == '<')
+ ret += "<";
+ else if (ch == '>')
+ ret += ">";
+ else
+ ret += ch;
+ }
+ } else if (!scanning_rich /* && !richtext */)
+ ret += ch;
+ // else the character is discarded, which will happen only if
+ // richtext == false and we are scanning rich text
+ val = val.substr(1);
+ }
+ return ret;
+}
+