consider TeX spacing conventions for punctuation marks
authorhaftmann
Mon Dec 01 12:16:59 2008 +0100 (2008-12-01)
changeset 28921e60a41c21768
parent 28920 4ed4b8b1988d
child 28922 ac2c34cad840
consider TeX spacing conventions for punctuation marks
doc-src/more_antiquote.ML
     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}"