diff options
| author | Prashanth Mundkur | 2019-01-16 15:15:40 -0800 |
|---|---|---|
| committer | Prashanth Mundkur | 2019-01-16 15:15:40 -0800 |
| commit | bb231219ff3d2d498d6f23f71ec1966dd58a304c (patch) | |
| tree | 1d847d1d44ad69fb40a552208968849e661452b0 /src | |
| parent | a5e2b3b7411f630b6d2337402330e13862b5666a (diff) | |
Latex: handle underscores when generating latex names.
Diffstat (limited to 'src')
| -rw-r--r-- | src/latex.ml | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/src/latex.ml b/src/latex.ml index 2f578f2c..56ba29ef 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -102,8 +102,7 @@ type id_category = | FunclNum of int | FunclApp of string -let replace_numbers str = - let replacements = +let number_replacements = [ ("0", "Zero"); ("1", "One"); ("2", "Two"); @@ -114,16 +113,27 @@ let replace_numbers str = ("7", "Seven"); ("8", "Eight"); ("9", "Nine") ] - in + +(* add to this as needed *) +let other_replacements = + [ ("_", "Underscore") ] + +let char_replace str replacements = List.fold_left (fun str (from, into) -> Str.global_replace (Str.regexp_string from) into str) str replacements +let replace_numbers str = + char_replace str number_replacements + +let replace_others str = + char_replace str other_replacements + let category_name = function | Function -> "fn" | Val -> "val" | Overload -> "overload" | FunclNum n -> "fcl" ^ unique_postfix n | FunclCtor (id, n) -> - let str = replace_numbers (Util.zencode_string (string_of_id id)) in + let str = replace_others (replace_numbers (Util.zencode_string (string_of_id id))) in "fcl" ^ String.sub str 1 (String.length str - 1) ^ unique_postfix n | FunclApp str -> "fcl" ^ str @@ -162,8 +172,8 @@ let latex_id id = (* If we have any other weird symbols in the id, remove them using Util.zencode_string (removing the z prefix) *) let str = Util.zencode_string str in let str = String.sub str 1 (String.length str - 1) in - (* Latex only allows letters in identifiers, so replace all numbers *) - let str = replace_numbers str in + (* Latex only allows letters in identifiers, so replace all numbers and other characters *) + let str = replace_others (replace_numbers str) in let generated = state.generated_names |> Bindings.bindings |> List.map snd |> StringSet.of_list in |
