regex_replace(to_utf8(repl_latex), s, "\\$(.*)\\$", "$1");
regex_replace(s, s, "\\\\\\[(.*)\\\\\\]", "$1");
repl_latex = from_utf8(s);
regex_replace(to_utf8(repl_latex), s, "\\$(.*)\\$", "$1");
regex_replace(s, s, "\\\\\\[(.*)\\\\\\]", "$1");
repl_latex = from_utf8(s);