src/Pure/General/position.ML
changeset 58854 b979c781c2db
parent 57899 5867d1306712
child 58978 e42da880c61e
equal deleted inserted replaced
58853:f8715e7c1be6 58854:b979c781c2db
    88 (* advance *)
    88 (* advance *)
    89 
    89 
    90 fun advance_count "\n" (i: int, j: int, k: int) =
    90 fun advance_count "\n" (i: int, j: int, k: int) =
    91       (if_valid i (i + 1), if_valid j (j + 1), k)
    91       (if_valid i (i + 1), if_valid j (j + 1), k)
    92   | advance_count s (i, j, k) =
    92   | advance_count s (i, j, k) =
    93       if Symbol.is_regular s then (i, if_valid j (j + 1), k)
    93       if Symbol.not_eof s then (i, if_valid j (j + 1), k)
    94       else (i, j, k);
    94       else (i, j, k);
    95 
    95 
    96 fun invalid_count (i, j, _: int) =
    96 fun invalid_count (i, j, _: int) =
    97   not (valid i orelse valid j);
    97   not (valid i orelse valid j);
    98 
    98