leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
225 stars 56 forks source link

Pdf should render inline code & unicode symbols #100

Open lakesare opened 1 year ago

lakesare commented 1 year ago
  1. Inline code should be more like this
image
  1. Some unicode symbols aren't getting rendered properly
image

Here is markdown on github for a comparison:

image
m4lvin commented 1 week ago

For 2. it seems there are only three missing unicode symbols, here is a list:

Missing character: There is no ➤ (U+27A4) in font DejaVuSerif:mode=node;script
Missing character: There is no 🎉 (U+1F389) in font DejaVuSerif:mode=node;scri
Missing character: There is no 💀 (U+1F480) in font DejaVuSerif:mode=node;scri
Missing character: There is no 💀 (U+1F480) in font DejaVuSansMono:mode=node;s
Missing character: There is no 🎉 (U+1F389) in font DejaVuSansMono/I:mode=node
Missing character: There is no 💀 (U+1F480) in font DejaVuSansMono:mode=node;s

(Obtained with cat out.log | grep "There is no" | uniq after compiling the .tex file.)

Two alternative ideas to solve this: