Replacement for merge request !357 (closed).
The number of commits has been substantially reduced by squashing.
The present version is ready for review.
Suggested reviewers: @p.-a.loizeau @v.friese @f.uhlig