semantics of white spaces

[affeldt-aist]

"This made me discover that coq2html is basically just removing the initial ( and trailing ) but keeps all the trailing whitespaces. I'm not sure we want this since two whitespaces, or more, have a specific semantics in markdown (force line break). This may lead to strange results, depending on the number of space before the final *) (which is something we don't control and which shouldn't have any meaning)." @proux01

[proux01]

To be more precise, this is about end of line whitespaces.

[affeldt-aist]

This is related to issue #32 and PR #37 proposes a solution

[proux01]

I doubt #37 fixes the issue (for instance when we don't have any space before *)). I don't know what's the best solution. The painful fact is that having *) aligned on the right margin forces user to put spaces before it, which clashes with \n being used by markdown for forced line break. So it seems we should either:

• drop mathcomp block style comments alltogether
• or if we want to keep them:
  • drop the ability to have forced line breaks (looks like the easiest solution, markdown follows line breaks in code blocks anyway, which is probably the only place we really need them, the implementation would just be wiping out all spaces at end of line before the final *))
  • put forced line breaks everywhere (probably a bit aggressive)

In any case, something has to be done, the current situation with ridiculous amounts of end of line spaces sometime forcing line breaks, sometime not, is pretty bad.