changed codeblocks comments to displays

src/plfa/backmatter/Fonts.lagda.md

@@ -11,113 +11,101 @@ module plfa.backmatter.Fonts where
 
 Preferably, all vertical bars should line up.
 
-```
-{-
---------------------------|
-abcdefghijklmnopqrstuvwxyz|
-ABCDEFGHIJKLMNOPQRSTUVWXYZ|
-ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
-ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
-ₐ   ₑ  ₕᵢⱼₖₗₘₙₒₚ ᵣₛₜᵤ  ₓ  |
---------------------------|
-----------|
-0123456789|
-⁰¹²³⁴⁵⁶⁷⁸⁹|
-₀₁₂₃₄₅₆₇₈₉|
-----------|
-------------------------|
-αβγδεζηθικλμνξοπρστυφχψω|
-ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
-------------------------|
-----|
-≠≠≠≠|
-ηημμ|
-ΓΓΔΔ|
-ΣΣΠΠ|
-λλλλ|
-ƛƛƛƛ|
-····|
-××××|
-ℓℓℓℓ|
-≡≡≡≡|
-¬¬¬¬|
-≤≤≥≥|
-∅∅∅∅|
-————|
-††‡‡|
-^^^^|
-''""|
-``~~|
-⊎⊎⊃⊃|
-∧∧∨∨|
-⊗⊗⊗⊗|
-⊔⊔⊔⊔|
-cᶜbᵇ|
-lˡrʳ|
-⁻⁻⁺⁺|
-ℕℕℕℕ|
-∀∀∃∃|
-′′″″|
-∘∘∘∘|
-‌≢≢≃≃|
-≲≲≳≳|
-≟≟≐≐|
-∸∸∸∸|
-⟨⟨⟩⟩|
-⌊⌊⌋⌋|
-⌈⌈⌉⌉|
-↑↑↓↓|
-⇔⇔↔↔|
-→→⇒⇒|
-←←⇐⇐|
-↞↞↠↠|
-∈∈∋∋|
-⊢⊢⊣⊣|
-⊥⊥⊤⊤|
-∷∷∷∷|
-∎∎∎∎|
-⦂⦂⦂⦂|
-∥∥∥∥|
-★★★★|
-∌∌∉∉|
-⨟⨟⨟⨟|
-⨆⨆⨆⨆|
-〔〔〕〕|
-----|
--}
-```
+    --------------------------|
+    abcdefghijklmnopqrstuvwxyz|
+    ABCDEFGHIJKLMNOPQRSTUVWXYZ|
+    ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
+    ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
+    ₐ   ₑ  ₕᵢⱼₖₗₘₙₒₚ ᵣₛₜᵤ  ₓ  |
+    --------------------------|
+    ----------|
+    0123456789|
+    ⁰¹²³⁴⁵⁶⁷⁸⁹|
+    ₀₁₂₃₄₅₆₇₈₉|
+    ----------|
+    ------------------------|
+    αβγδεζηθικλμνξοπρστυφχψω|
+    ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
+    ------------------------|
+    ----|
+    ≠≠≠≠|
+    ηημμ|
+    ΓΓΔΔ|
+    ΣΣΠΠ|
+    λλλλ|
+    ƛƛƛƛ|
+    ····|
+    ××××|
+    ℓℓℓℓ|
+    ≡≡≡≡|
+    ¬¬¬¬|
+    ≤≤≥≥|
+    ∅∅∅∅|
+    ————|
+    ††‡‡|
+    ^^^^|
+    ''""|
+    ``~~|
+    ⊎⊎⊃⊃|
+    ∧∧∨∨|
+    ⊗⊗⊗⊗|
+    ⊔⊔⊔⊔|
+    cᶜbᵇ|
+    lˡrʳ|
+    ⁻⁻⁺⁺|
+    ℕℕℕℕ|
+    ∀∀∃∃|
+    ′′″″|
+    ∘∘∘∘|
+    ‌≢≢≃≃|
+    ≲≲≳≳|
+    ≟≟≐≐|
+    ∸∸∸∸|
+    ⟨⟨⟩⟩|
+    ⌊⌊⌋⌋|
+    ⌈⌈⌉⌉|
+    ↑↑↓↓|
+    ⇔⇔↔↔|
+    →→⇒⇒|
+    ←←⇐⇐|
+    ↞↞↠↠|
+    ∈∈∋∋|
+    ⊢⊢⊣⊣|
+    ⊥⊥⊤⊤|
+    ∷∷∷∷|
+    ∎∎∎∎|
+    ⦂⦂⦂⦂|
+    ∥∥∥∥|
+    ★★★★|
+    ∌∌∉∉|
+    ⨟⨟⨟⨟|
+    ⨆⨆⨆⨆|
+    〔〔〕〕|
+    ----|
 
 In the book we use the em-dash to make big arrows.
 
-```
-{-
-----|
-—→—→|
-←—←—|
-↞—↞—|
-—↠—↠|
-----|
--}
-```
+    ----|
+    —→—→|
+    ←—←—|
+    ↞—↞—|
+    —↠—↠|
+    ----|
 
 Here are some characters that are often not monospaced.
 
-```
-{-
-----|
-😇😇|
-😈😈|
-⁗⁗|
-‴‴|
-----|
-------------|
-------------|
-----------|
-𝔸𝔹𝔻𝔼𝔽𝔾𝕀𝕁𝕂𝕃𝕄ℕ𝕆𝕊|
-𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛|
-𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘|
-ℰℱ|
-----------|
+    ----|
+    😇😇|
+    😈😈|
+    ⁗⁗|
+    ‴‴|
+    ----|
+    ------------|
+    ------------|
+    ----------|
+    𝔸𝔹𝔻𝔼𝔽𝔾𝕀𝕁𝕂𝕃𝕄ℕ𝕆𝕊|
+    𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛|
+    𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘|
+    ℰℱ|
+    ----------|
 
--}
-```