doc-src/more_antiquote.ML
changeset 28921 e60a41c21768
parent 28727 185110a4b97a
child 29397 aab26a65e80f
equal deleted inserted replaced
28920:4ed4b8b1988d 28921:e60a41c21768
    20 fun typewriter s =
    20 fun typewriter s =
    21   let
    21   let
    22     val parse = Scan.repeat
    22     val parse = Scan.repeat
    23       (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
    23       (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
    24         || (Scan.this_string " " 
    24         || (Scan.this_string " " 
       
    25           || Scan.this_string "."
       
    26           || Scan.this_string ","
    25           || Scan.this_string ":"
    27           || Scan.this_string ":"
       
    28           || Scan.this_string ";"
    26           || Scan.this_string "\"" |-- Scan.succeed "{\\char34}"
    29           || Scan.this_string "\"" |-- Scan.succeed "{\\char34}"
    27           || Scan.this_string "#" |-- Scan.succeed "{\\char35}"
    30           || Scan.this_string "#" |-- Scan.succeed "{\\char35}"
    28           || Scan.this_string "$" |-- Scan.succeed "{\\char36}"
    31           || Scan.this_string "$" |-- Scan.succeed "{\\char36}"
    29           || Scan.this_string "%" |-- Scan.succeed "{\\char37}"
    32           || Scan.this_string "%" |-- Scan.succeed "{\\char37}"
    30           || Scan.this_string "&" |-- Scan.succeed "{\\char38}"
    33           || Scan.this_string "&" |-- Scan.succeed "{\\char38}"