Simplified plta.Fonts page

2018-06-26 15:01:29 +01:00 · 2018-06-26 15:01:29 +01:00 · e819aee20a
commit e819aee20a
parent e74965be3d
1 changed files with 10 additions and 41 deletions
--- a/src/plta/Fonts.lagda
+++ b/src/plta/Fonts.lagda
@ -10,8 +10,6 @@ module plta.Fonts where

 Test page for fonts. All vertical bars should line up.

-Agda:
-
 \begin{code}
 {-
 abcdefghijklmnopqrstuvwxyz|
@ -19,15 +17,19 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
 ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
 ₐ   ₑ   ᵢⱼ    ₒ  ᵣ  ᵤ  ₓ  |
+
 αβγδεφικλμνωπψρστυχξζ|
 ΑΒΓΔΕΦΙΚΛΜΝΩΠΨΡΣΤΥΧΞΖ|
+
 0123456789|
 ⁰¹²³⁴⁵⁶⁷⁸⁹|
 ₀₁₂₃₄₅₆₇₈₉|
+
 ⟨⟨⟨⟩⟩⟩|
 →→→⇒⇒⇒|
 ←←←⇐⇐⇐|
 ------|
+
 ⌊⌋⌈⌉|
 →→→→|
 ↦↦↦↦|
@ -37,44 +39,11 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 ∈∈∈∈|
 ∋∋∋∋|
 ----|
------------
-⟶⟶⟶⟶
-⟹⟹⟹⟹
------------
-𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛
-𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘
+
+⟶⟶⟶⟶|
+⟹⟹⟹⟹|
+
+𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛|
+𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘|
 -}
 \end{code}
-
-Indented code:
-
-    abcdefghijklmnopqrstuvwxyz|
-    ABCDEFGHIJKLMNOPQRSTUVWXYZ|
-    ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
-    ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
-    ₐ   ₑ   ᵢⱼ    ₒ  ᵣ  ᵤ  ₓ  |
-    αβγδεφικλμνωπψρστυχξζ|
-    ΑΒΓΔΕΦΙΚΛΜΝΩΠΨΡΣΤΥΧΞΖ|
-    0123456789|
-    ⁰¹²³⁴⁵⁶⁷⁸⁹|
-    ₀₁₂₃₄₅₆₇₈₉|
-    ⟨⟨⟨⟩⟩⟩|
-    →→→⇒⇒⇒|
-    ←←←⇐⇐⇐|
-    ------|
-    ⌊⌋⌈⌉|
-    →→→→|
-    ↦↦↦↦|
-    ↠↠↠↠|
-    ⊢⊢⊢⊢|
-    ⊣⊣⊣⊣|
-    ∈∈∈∈|
-    ∋∋∋∋|
-    ----|
-    ------------
-    ⟶⟶⟶⟶
-    ⟹⟹⟹⟹
-    ------------
-    𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛
-    𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘
-