jbe/bsw@0: function parse._pre_fold(str)
jbe/bsw@0:   local str = str
jbe/bsw@0:   local special_chars = charset.get_data().special_chars
jbe/bsw@0:   local function replace(name, dst)
jbe/bsw@0:     local src = special_chars[name]
jbe/bsw@0:     if src then
jbe/bsw@0:       local pattern = string.gsub(src, "[][()^$%%]", "%%%1")
jbe/bsw@0:       str = string.gsub(str, pattern, dst)
jbe/bsw@0:     end
jbe/bsw@0:   end
jbe/bsw@0:   replace("nobreak_space",  " ")
jbe/bsw@0:   replace("minus_sign",     "-")
jbe/bsw@0:   replace("hyphen_sign",    "-")
jbe/bsw@0:   replace("nobreak_hyphen", "-")
jbe/bsw@0:   replace("figure_dash",    "-")
jbe/bsw@0:   str = string.gsub(str, "\t+", " ")
jbe/bsw@0:   str = string.gsub(str, "^ +", "")
jbe/bsw@0:   str = string.gsub(str, " +$", "")
jbe/bsw@0:   str = string.gsub(str, " +", " ")
jbe/bsw@0:   return str
jbe/bsw@0: end