| changeset 58727 | e3d0a6a012eb |
| parent 58716 | 23a380cc45f4 |
| child 58861 | 5ff61774df11 |
| 58726:cee57ab1f76f | 58727:e3d0a6a012eb |
|---|---|
37 translate_string |
37 translate_string |
38 (fn " " => "\\ " |
38 (fn " " => "\\ " |
39 | "\t" => "\\ " |
39 | "\t" => "\\ " |
40 | "\n" => "\\isanewline\n" |
40 | "\n" => "\\isanewline\n" |
41 | s => |
41 | s => |
42 if exists_string (fn s' => s = s') "#$%^&_{}~\\" |
42 if exists_string (fn s' => s = s') "#$%^&_{}~\\<>" |
43 then enclose "{\\char`\\" "}" s else s); |
43 then enclose "{\\char`\\" "}" s else s); |
44 |
44 |
45 |
45 |
46 (* symbol output *) |
46 (* symbol output *) |
47 |
47 |