# HG changeset patch
# User haftmann
# Date 1228130219 -3600
# Node ID e60a41c217688b55c3b2fd91d4dc553be0468b59
# Parent  4ed4b8b1988d1513e8b2446a65a73dfd12b9b433
consider TeX spacing conventions for punctuation marks

diff -r 4ed4b8b1988d -r e60a41c21768 doc-src/more_antiquote.ML
--- 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}"