--- a/doc-src/more_antiquote.ML Sun Nov 30 18:10:00 2008 +0100
+++ b/doc-src/more_antiquote.ML Mon Dec 01 12:16:59 2008 +0100
@@ -22,7 +22,10 @@
val parse = Scan.repeat
(Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
|| (Scan.this_string " "
+ || Scan.this_string "."
+ || Scan.this_string ","
|| Scan.this_string ":"
+ || Scan.this_string ";"
|| Scan.this_string "\"" |-- Scan.succeed "{\\char34}"
|| Scan.this_string "#" |-- Scan.succeed "{\\char35}"
|| Scan.this_string "$" |-- Scan.succeed "{\\char36}"