26 local |
26 local |
27 |
27 |
28 val output_chr = fn |
28 val output_chr = fn |
29 " " => "\\ " | |
29 " " => "\\ " | |
30 "\n" => "\\isanewline\n" | |
30 "\n" => "\\isanewline\n" | |
31 "$" => "\\$" | |
31 "#" => "{\\isacharhash}" | |
32 "&" => "\\&" | |
32 "$" => "{\\isachardollar}" | |
33 "%" => "\\%" | |
33 "%" => "{\\isacharpercent}" | |
34 "#" => "\\#" | |
34 "&" => "{\\isacharampersand}" | |
35 "_" => "\\_" | |
35 "'" => "{\\isacharprime}" | |
36 "{" => "{\\isabraceleft}" | |
36 "(" => "{\\isacharparenleft}" | |
37 "}" => "{\\isabraceright}" | |
37 ")" => "{\\isacharparenright}" | |
38 "~" => "{\\isatilde}" | |
38 "*" => "{\\isacharasterisk}" | |
39 "^" => "{\\isacircum}" | |
39 "-" => "{\\isacharminus}" | |
40 "\"" => "{\"}" | |
40 "<" => "{\\isacharless}" | |
41 "\\" => "{\\isabackslash}" | |
41 ">" => "{\\isachargreater}" | |
|
42 "[" => "{\\isacharbrackleft}" | |
|
43 "\"" => "{\\isachardoublequote}" | |
|
44 "\\" => "{\\isacharbackslash}" | |
|
45 "]" => "{\\isacharbrackright}" | |
|
46 "^" => "{\\isacharcircum}" | |
|
47 "_" => "{\\isacharunderscore}" | |
|
48 "{" => "{\\isacharbraceleft}" | |
|
49 "|" => "{\\isacharbar}" | |
|
50 "}" => "{\\isacharbraceright}" | |
|
51 "~" => "{\\isachartilde}" | |
42 c => c; |
52 c => c; |
43 |
53 |
44 fun output_sym s = |
54 fun output_sym s = |
45 if size s = 1 then output_chr s |
55 if size s = 1 then output_chr s |
46 else |
56 else |