(unfortunately) nobody cares that reversible parsing actually works.
Well what about https://github.com/kolmodin/binary/blob/master/tests/QC.hs#L50 is this not "caring for reversibility"? (in a similar context)
we cannot be sure about determinism
Assume you come up with a deterministic grammar for Isabelle (say). How do you want to be sure it is the right one? Would it not be a good idea to use the given grammar (extract from sources of tools, e.g., https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/Isar... - this is already a combinator parser? or from specification/documentation, e.g., http://isabelle.in.tum.de/dist/Isabelle2020/doc/isar-ref.pdf ?) Best regards, J. NB: full Isabelle seems quite the challenge to parse: isar-ref 8.4.5 "... parsing may be ambiguous. Isabelle lets the Earley parser enumerate all possible parse trees... Terms that cannot be type-checked are filtered out. Unlike regular type reconstruction, ... the filtering stage only ..."