Thanks to Pavel, we now have a solution that both of us will like. E.g., the new approach is illustrated in #848. I am working on implementing this solution here too.