michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Reset fonts; added Greek Letter Heta to the list of characters in plta.Fonts

Browse source
This commit is contained in:
Wen Kokke 2018-06-26 16:17:25 +01:00
parent e819aee20a
commit 7a3676ae2e
2 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
_sass/agda.scss
View file

@ -1,7 +1,7 @@
// Define variables for code formatting // Define variables for code formatting
@mixin code-font { @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; font-size: .85em;
} }
@mixin code-container { @mixin code-container {

12
src/plta/Fonts.lagda
View file

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