@@ -494,7 +494,7 @@ escapedChar = do
494-- ignore standalone, nonescaped special characters
494-- ignore standalone, nonescaped special characters
495unescapedChar = oneOf "`$^&_#{}|<>" >> return (Str "")
495unescapedChar = oneOf "`$^&_#{}|<>" >> return (Str "")
497−specialChar = choice [ backslash, tilde, caret, bar, lt, gt ]
497+specialChar = choice [ backslash, tilde, caret, bar, lt, gt, doubleQuote ]
499backslash = try (string "\\textbackslash") >> return (Str "\\")
499backslash = try (string "\\textbackslash") >> return (Str "\\")
@@ -508,6 +508,8 @@ lt = try (string "\\textless") >> return (Str "<")
509gt = try (string "\\textgreater") >> return (Str ">")
509gt = try (string "\\textgreater") >> return (Str ">")
511+doubleQuote = char '"' >> return (Str "\"")
511code = code1 <|> code2
513code = code1 <|> code2
513code1 = try $ do
515code1 = try $ do