--- a/src/Pure/Thy/latex.ML Sat Aug 19 12:48:26 2000 +0200
+++ b/src/Pure/Thy/latex.ML Sat Aug 19 12:49:19 2000 +0200
@@ -28,17 +28,27 @@
val output_chr = fn
" " => "\\ " |
"\n" => "\\isanewline\n" |
- "$" => "\\$" |
- "&" => "\\&" |
- "%" => "\\%" |
- "#" => "\\#" |
- "_" => "\\_" |
- "{" => "{\\isabraceleft}" |
- "}" => "{\\isabraceright}" |
- "~" => "{\\isatilde}" |
- "^" => "{\\isacircum}" |
- "\"" => "{\"}" |
- "\\" => "{\\isabackslash}" |
+ "#" => "{\\isacharhash}" |
+ "$" => "{\\isachardollar}" |
+ "%" => "{\\isacharpercent}" |
+ "&" => "{\\isacharampersand}" |
+ "'" => "{\\isacharprime}" |
+ "(" => "{\\isacharparenleft}" |
+ ")" => "{\\isacharparenright}" |
+ "*" => "{\\isacharasterisk}" |
+ "-" => "{\\isacharminus}" |
+ "<" => "{\\isacharless}" |
+ ">" => "{\\isachargreater}" |
+ "[" => "{\\isacharbrackleft}" |
+ "\"" => "{\\isachardoublequote}" |
+ "\\" => "{\\isacharbackslash}" |
+ "]" => "{\\isacharbrackright}" |
+ "^" => "{\\isacharcircum}" |
+ "_" => "{\\isacharunderscore}" |
+ "{" => "{\\isacharbraceleft}" |
+ "|" => "{\\isacharbar}" |
+ "}" => "{\\isacharbraceright}" |
+ "~" => "{\\isachartilde}" |
c => c;
fun output_sym s =