src/Pure/Syntax/syn_ext.ML
changeset 21858 05f57309170c
parent 21772 7c7ade4f537b
child 22573 2ac646ab2f6c
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -203,11 +203,11 @@
     1.4  val scan_sym =
     1.5    $$ "_" >> K (Argument ("", 0)) ||
     1.6    $$ "\\<index>" >> K index ||
     1.7 -  $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o read_int) ||
     1.8 +  $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
     1.9    $$ ")" >> K En ||
    1.10    $$ "/" -- $$ "/" >> K (Brk ~1) ||
    1.11 -  $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
    1.12 -  Scan.any1 Symbol.is_blank >> (Space o implode) ||
    1.13 +  $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
    1.14 +  Scan.many1 Symbol.is_blank >> (Space o implode) ||
    1.15    Scan.repeat1 scan_delim_char >> (Delim o implode);
    1.16  
    1.17  val scan_symb =