1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/framework/env/parse/_pre_fold.lua	Sun Oct 25 12:00:00 2009 +0100
     1.3 @@ -0,0 +1,21 @@
     1.4 +function parse._pre_fold(str)
     1.5 +  local str = str
     1.6 +  local special_chars = charset.get_data().special_chars
     1.7 +  local function replace(name, dst)
     1.8 +    local src = special_chars[name]
     1.9 +    if src then
    1.10 +      local pattern = string.gsub(src, "[][()^$%%]", "%%%1")
    1.11 +      str = string.gsub(str, pattern, dst)
    1.12 +    end
    1.13 +  end
    1.14 +  replace("nobreak_space",  " ")
    1.15 +  replace("minus_sign",     "-")
    1.16 +  replace("hyphen_sign",    "-")
    1.17 +  replace("nobreak_hyphen", "-")
    1.18 +  replace("figure_dash",    "-")
    1.19 +  str = string.gsub(str, "\t+", " ")
    1.20 +  str = string.gsub(str, "^ +", "")
    1.21 +  str = string.gsub(str, " +$", "")
    1.22 +  str = string.gsub(str, " +", " ")
    1.23 +  return str
    1.24 +end