PDF from lean code

Stream: lean4

[Rafa M Munoz-Grenier]

Is there a systematic way to convert Lean code into a nicely formatted pdf, like that in MIL? I'm also curious about emulating the documentation view of MIL into my current project, so that my project would be able to display html in the doc view.