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