changeset 61578 | 6623c81cb15a |
parent 61516 | 8e3705d91cfa |
child 61595 | 3591274c607e |
61577:de7045616fc7 | 61578:6623c81cb15a |
---|---|
34 translate_string |
34 translate_string |
35 (fn " " => "\\ " |
35 (fn " " => "\\ " |
36 | "\t" => "\\ " |
36 | "\t" => "\\ " |
37 | "\n" => "\\isanewline\n" |
37 | "\n" => "\\isanewline\n" |
38 | s => |
38 | s => |
39 if exists_string (fn s' => s = s') "\"#$%&'<>\\^_{}~" |
39 if exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" |
40 then enclose "{\\char`\\" "}" s else s); |
40 then enclose "{\\char`\\" "}" s else s); |
41 |
41 |
42 |
42 |
43 (* output symbols *) |
43 (* output symbols *) |
44 |
44 |