diff --git a/_sass/agda.scss b/_sass/agda.scss index b26257fb..560a0611 100644 --- a/_sass/agda.scss +++ b/_sass/agda.scss @@ -1,7 +1,7 @@ // Define variables for code formatting @mixin code-font { - font-family: 'Source Code Pro', 'Courier New', 'DejaVu Sans Mono', 'Bitstream Vera Sans Mono', 'Menlo', 'Consolas', 'Monaco', 'Ludica Console', 'Liberation Mono', 'Courier New', monospace, serif; + font-family: 'Source Code Pro', 'DejaVu Sans Mono', 'Bitstream Vera Sans Mono', 'Menlo', 'Consolas', 'Monaco', 'Ludica Console', 'Liberation Mono', 'Courier New', monospace, serif; font-size: .85em; } @mixin code-container { diff --git a/src/plta/Fonts.lagda b/src/plta/Fonts.lagda index 9e614ca4..79832229 100644 --- a/src/plta/Fonts.lagda +++ b/src/plta/Fonts.lagda @@ -12,37 +12,45 @@ Test page for fonts. All vertical bars should line up. \begin{code} {- +--------------------------| abcdefghijklmnopqrstuvwxyz| ABCDEFGHIJKLMNOPQRSTUVWXYZ| ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ| ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ | ₐ ₑ ᵢⱼ ₒ ᵣ ᵤ ₓ | +---------------------| αβγδεφικλμνωπψρστυχξζ| ΑΒΓΔΕΦΙΚΛΜΝΩΠΨΡΣΤΥΧΞΖ| +----------| 0123456789| ⁰¹²³⁴⁵⁶⁷⁸⁹| ₀₁₂₃₄₅₆₇₈₉| +------| ⟨⟨⟨⟩⟩⟩| →→→⇒⇒⇒| ←←←⇐⇐⇐| ------| +----| ⌊⌋⌈⌉| →→→→| ↦↦↦↦| ↠↠↠↠| -⊢⊢⊢⊢| -⊣⊣⊣⊣| +ͰͰͰͰ| ∈∈∈∈| ∋∋∋∋| ----| +⊢⊢⊢⊢| +⊣⊣⊣⊣| +--------| ⟶⟶⟶⟶| ⟹⟹⟹⟹| +----------| 𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛| 𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘| -}