equal
deleted
inserted
replaced
879 strip_blanks (s1 :: s2 :: ss) |
879 strip_blanks (s1 :: s2 :: ss) |
880 | strip_blanks (s :: ss) = s :: strip_blanks ss |
880 | strip_blanks (s :: ss) = s :: strip_blanks ss |
881 |
881 |
882 val scan_nat = |
882 val scan_nat = |
883 Scan.repeat1 (Scan.one Symbol.is_ascii_digit) |
883 Scan.repeat1 (Scan.one Symbol.is_ascii_digit) |
884 >> (the o Int.fromString o space_implode "") |
884 >> (the o Int.fromString o implode) |
885 val scan_rel_name = |
885 val scan_rel_name = |
886 ($$ "s" |-- scan_nat >> pair 1 |
886 ($$ "s" |-- scan_nat >> pair 1 |
887 || $$ "r" |-- scan_nat >> pair 2 |
887 || $$ "r" |-- scan_nat >> pair 2 |
888 || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'") |
888 || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'") |
889 >> (fn ((n, j), SOME _) => (n, ~j - 1) |
889 >> (fn ((n, j), SOME _) => (n, ~j - 1) |