fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end

special code with lists no longer necessary, use sets

proper error prefixes;

more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;

tuned message;

clarified Linear_Set.next/prev: check definedness;

merged

Improved complete lattice formalisation - no more index set.

merged

tuned proofs;