> This would save an enormous amount of space, and make things far more tidy.
Why? The output pdf is typically smaller than the input that produces it. Using rendered pdfs seems simple and very natural, and at worst can use twice the total amount of space.
Instead of storing both pdf and source text, just store the source. The pdf is generated on demand, in whatever style you like.
Although, I had no idea PDFs were smaller than the input. I thought that they were substantially larger actually. But regardless, storing things twice is wasteful.
Why? The output pdf is typically smaller than the input that produces it. Using rendered pdfs seems simple and very natural, and at worst can use twice the total amount of space.