doc-src/more_antiquote.ML
changeset 28921 e60a41c21768
parent 28727 185110a4b97a
child 29394 aab26a65e80f
     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}"