diff --git a/README.md b/README.md index de9e45238..b283de90a 100644 --- a/README.md +++ b/README.md @@ -145,16 +145,18 @@ Since version 2.6.0, Agda has had support for literate editing with Markdown, us If you already have settings which change your `auto-mode-alist` in your configuration, put these _after_ the ones you already have or combine them if you are comfortable with Emacs Lisp. The configuration file for Emacs is normally located in `HOME/.emacs` or `HOME/.emacs.d/init.el`, but Aquamacs users might need to move their startup settings to the “Preferences.el” file in `HOME/Library/Preferences/Aquamacs Emacs/Preferences`. For Windows, see [the GNU Emacs documentation][emacs-home] for a description of where the Emacs configuration is located. -#### Optional: using the mononoki font with Emacs +#### Optional: using the JuliaMono font with Emacs -Agda uses Unicode characters for many key symbols, and it is important that the font which you use to view and edit Agda programs shows these symbols correctly. The most important part is that the font you use has good Unicode support, so while we recommend [mononoki][font-mononoki], fonts such as [Source Code Pro][font-sourcecodepro], [DejaVu Sans Mono][font-dejavusansmono], and [FreeMono][font-freemono] are all good alternatives. +Agda uses Unicode characters for many key symbols, and it is important that the font which you use to view and edit Agda programs shows these symbols correctly. The most important part is that the font you use has good Unicode support, so while we recommend [JuliaMono][font-JuliaMono], fonts such as [mononoki][font-mononoki], [Source Code Pro][font-sourcecodepro], [DejaVu Sans Mono][font-dejavusansmono], and [FreeMono][font-freemono] are all good alternatives. -You can download and install mononoki directly from [the website][font-mononoki]. For most systems, installing a font is merely a matter of clicking the downloaded `.otf` or `.ttf` file. If your package manager offers a package for mononoki, that might be easier. For instance, Homebrew on macOS offers the `font-mononoki` package, and APT on Debian offers the `fonts-mononoki` package. To configure Emacs to use mononoki as its default font, add the following to the end of your Emacs configuration file: +You can download and install JuliaMono directly from [the website][font-JuliaMono]. For most systems, installing a font is merely a matter of clicking the downloaded `.otf` or `.ttf` file. +If your package manager offers a package for JuliaMono, that might be easier. For instance, Homebrew on macOS offers the [`font-juliamono`][[font-JuliaMono-homebrew]] cask. +To configure Emacs to use JuliaMono as its default font, add the following to the end of your Emacs configuration file: ```elisp -;; default to mononoki +;; default to JuliaMono (set-face-attribute 'default nil - :family "mononoki" + :family "JuliaMono" :height 120 :weight 'normal :width 'normal) @@ -290,6 +292,8 @@ If you plan to build PLFA locally, please refer to [Contributing][plfa-contribut [vscode-agda]: https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode [font-sourcecodepro]: https://github.com/adobe-fonts/source-code-pro [font-dejavusansmono]: https://dejavu-fonts.github.io/ +[font-JuliaMono]: https://juliamono.netlify.app/download/ +[font-JuliaMono-homebrew]: https://juliamono.netlify.app/download/#macos_homebrew [font-freemono]: https://www.gnu.org/software/freefont/ [font-mononoki]: https://madmalik.github.io/mononoki/ [font-mononoki-debian]: https://packages.debian.org/sid/fonts/fonts-mononoki diff --git a/book/epub/fonts/DejaVuMathTeXGyre.ttf b/book/epub/fonts/DejaVuMathTeXGyre.ttf deleted file mode 100644 index 8a24f0640..000000000 Binary files a/book/epub/fonts/DejaVuMathTeXGyre.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSans-Bold.ttf b/book/epub/fonts/DejaVuSans-Bold.ttf deleted file mode 100644 index 6d65fa7dc..000000000 Binary files a/book/epub/fonts/DejaVuSans-Bold.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSans-BoldOblique.ttf b/book/epub/fonts/DejaVuSans-BoldOblique.ttf deleted file mode 100644 index 753f2d80b..000000000 Binary files a/book/epub/fonts/DejaVuSans-BoldOblique.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSans-ExtraLight.ttf b/book/epub/fonts/DejaVuSans-ExtraLight.ttf deleted file mode 100644 index b09f32d7d..000000000 Binary files a/book/epub/fonts/DejaVuSans-ExtraLight.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSans-Oblique.ttf b/book/epub/fonts/DejaVuSans-Oblique.ttf deleted file mode 100644 index 999bac771..000000000 Binary files a/book/epub/fonts/DejaVuSans-Oblique.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSans-Regular.ttf b/book/epub/fonts/DejaVuSans-Regular.ttf deleted file mode 100644 index e5f7eecce..000000000 Binary files a/book/epub/fonts/DejaVuSans-Regular.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSansMono-Bold.ttf b/book/epub/fonts/DejaVuSansMono-Bold.ttf deleted file mode 100644 index 8184ced8c..000000000 Binary files a/book/epub/fonts/DejaVuSansMono-Bold.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSansMono-BoldOblique.ttf b/book/epub/fonts/DejaVuSansMono-BoldOblique.ttf deleted file mode 100644 index 754dca732..000000000 Binary files a/book/epub/fonts/DejaVuSansMono-BoldOblique.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSansMono-Oblique.ttf b/book/epub/fonts/DejaVuSansMono-Oblique.ttf deleted file mode 100644 index 4c858d401..000000000 Binary files a/book/epub/fonts/DejaVuSansMono-Oblique.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSansMono-Regular.ttf b/book/epub/fonts/DejaVuSansMono-Regular.ttf deleted file mode 100644 index f5786022f..000000000 Binary files a/book/epub/fonts/DejaVuSansMono-Regular.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSerif-Bold.ttf b/book/epub/fonts/DejaVuSerif-Bold.ttf deleted file mode 100644 index 3bb755fa1..000000000 Binary files a/book/epub/fonts/DejaVuSerif-Bold.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSerif-BoldItalic.ttf b/book/epub/fonts/DejaVuSerif-BoldItalic.ttf deleted file mode 100644 index a36dd4b70..000000000 Binary files a/book/epub/fonts/DejaVuSerif-BoldItalic.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSerif-Italic.ttf b/book/epub/fonts/DejaVuSerif-Italic.ttf deleted file mode 100644 index 805daf222..000000000 Binary files a/book/epub/fonts/DejaVuSerif-Italic.ttf and /dev/null differ diff --git a/book/epub/fonts/DejaVuSerif-Regular.ttf b/book/epub/fonts/DejaVuSerif-Regular.ttf deleted file mode 100644 index 0b803d206..000000000 Binary files a/book/epub/fonts/DejaVuSerif-Regular.ttf and /dev/null differ diff --git a/book/epub/fonts/Frankenfont-Regular.ttf b/book/epub/fonts/Frankenfont-Regular.ttf deleted file mode 100644 index 990c96ec6..000000000 Binary files a/book/epub/fonts/Frankenfont-Regular.ttf and /dev/null differ diff --git a/book/epub/fonts/FreeMono-Bold.ttf b/book/epub/fonts/FreeMono-Bold.ttf deleted file mode 100644 index 48154499c..000000000 Binary files a/book/epub/fonts/FreeMono-Bold.ttf and /dev/null differ diff --git a/book/epub/fonts/FreeMono-BoldOblique.ttf b/book/epub/fonts/FreeMono-BoldOblique.ttf deleted file mode 100644 index 02692e1a3..000000000 Binary files a/book/epub/fonts/FreeMono-BoldOblique.ttf and /dev/null differ diff --git a/book/epub/fonts/FreeMono-Oblique.ttf b/book/epub/fonts/FreeMono-Oblique.ttf deleted file mode 100644 index 87caa0ff1..000000000 Binary files a/book/epub/fonts/FreeMono-Oblique.ttf and /dev/null differ diff --git a/book/epub/fonts/FreeMono-Regular.ttf b/book/epub/fonts/FreeMono-Regular.ttf deleted file mode 100644 index ff5cc0e9b..000000000 Binary files a/book/epub/fonts/FreeMono-Regular.ttf and /dev/null differ diff --git a/book/epub/fonts/JuliaMono-Bold.ttf b/book/epub/fonts/JuliaMono-Bold.ttf new file mode 100644 index 000000000..b1794a309 Binary files /dev/null and b/book/epub/fonts/JuliaMono-Bold.ttf differ diff --git a/book/epub/fonts/JuliaMono-Bold.woff2 b/book/epub/fonts/JuliaMono-Bold.woff2 new file mode 100644 index 000000000..4c9d30b48 Binary files /dev/null and b/book/epub/fonts/JuliaMono-Bold.woff2 differ diff --git a/book/epub/fonts/JuliaMono-BoldItalic.ttf b/book/epub/fonts/JuliaMono-BoldItalic.ttf new file mode 100644 index 000000000..86eb646b3 Binary files /dev/null and b/book/epub/fonts/JuliaMono-BoldItalic.ttf differ diff --git a/book/epub/fonts/JuliaMono-BoldItalic.woff2 b/book/epub/fonts/JuliaMono-BoldItalic.woff2 new file mode 100644 index 000000000..170e8aa0f Binary files /dev/null and b/book/epub/fonts/JuliaMono-BoldItalic.woff2 differ diff --git a/book/epub/fonts/JuliaMono-Regular.ttf b/book/epub/fonts/JuliaMono-Regular.ttf new file mode 100644 index 000000000..a47c0ede8 Binary files /dev/null and b/book/epub/fonts/JuliaMono-Regular.ttf differ diff --git a/book/epub/fonts/JuliaMono-Regular.woff2 b/book/epub/fonts/JuliaMono-Regular.woff2 new file mode 100644 index 000000000..3a5e27f0b Binary files /dev/null and b/book/epub/fonts/JuliaMono-Regular.woff2 differ diff --git a/book/epub/fonts/JuliaMono-RegularItalic.ttf b/book/epub/fonts/JuliaMono-RegularItalic.ttf new file mode 100644 index 000000000..d9dd2b74e Binary files /dev/null and b/book/epub/fonts/JuliaMono-RegularItalic.ttf differ diff --git a/book/epub/fonts/JuliaMono-RegularItalic.woff2 b/book/epub/fonts/JuliaMono-RegularItalic.woff2 new file mode 100644 index 000000000..007a2625f Binary files /dev/null and b/book/epub/fonts/JuliaMono-RegularItalic.woff2 differ diff --git a/book/epub/fonts/mononoki-Bold.ttf b/book/epub/fonts/mononoki-Bold.ttf deleted file mode 100644 index 407ed3edf..000000000 Binary files a/book/epub/fonts/mononoki-Bold.ttf and /dev/null differ diff --git a/book/epub/fonts/mononoki-BoldItalic.ttf b/book/epub/fonts/mononoki-BoldItalic.ttf deleted file mode 100644 index 784c2d053..000000000 Binary files a/book/epub/fonts/mononoki-BoldItalic.ttf and /dev/null differ diff --git a/book/epub/fonts/mononoki-Italic.ttf b/book/epub/fonts/mononoki-Italic.ttf deleted file mode 100644 index dad4dcc5f..000000000 Binary files a/book/epub/fonts/mononoki-Italic.ttf and /dev/null differ diff --git a/book/epub/fonts/mononoki-Regular.ttf b/book/epub/fonts/mononoki-Regular.ttf deleted file mode 100644 index 9510ac85d..000000000 Binary files a/book/epub/fonts/mononoki-Regular.ttf and /dev/null differ diff --git a/book/epub/sass/theme/agda.scss b/book/epub/sass/theme/agda.scss index 552fabe78..d92db3ab7 100644 --- a/book/epub/sass/theme/agda.scss +++ b/book/epub/sass/theme/agda.scss @@ -1,5 +1,5 @@ @mixin code-font { - font-family: 'Frankenfont', 'FreeMono', 'DejaVu Sans Mono', 'mononoki', 'Source Code Pro', monospace; + font-family: 'JuliaMono'; font-size: .85em; } @mixin code-container { @@ -29,7 +29,7 @@ pre.Spec { .Number { color: #A020F0 } .Symbol { color: #404040 } .PrimitiveType { color: #0000CD } -.Operator {} +// .Operator {} /* NameKinds. */ .Bound { color: black } @@ -44,7 +44,7 @@ pre.Spec { .Record { color: #0000CD } /* OtherAspects. */ -.DottedPattern {} +// .DottedPattern {} .UnsolvedMeta { color: black; background: yellow } .UnsolvedConstraint { color: black; background: yellow } .TerminationProblem { color: black; background: #FFA07A } diff --git a/book/epub/sass/theme/epub.scss b/book/epub/sass/theme/epub.scss index f7d4ab14e..84b8e7b5c 100644 --- a/book/epub/sass/theme/epub.scss +++ b/book/epub/sass/theme/epub.scss @@ -1,6 +1,6 @@ /* This defines styles and classes used in the book */ body { margin: 5%; text-align: justify; font-size: medium; } -code { font-family: monospace; } +code { font-family: 'JuliaMono'; } h1 { text-align: left; } h2 { text-align: left; } h3 { text-align: left; } @@ -8,9 +8,9 @@ h4 { text-align: left; } h5 { text-align: left; } h6 { text-align: left; } /* For title, author, and date on the cover page */ -h1.title { } -p.author { } -p.date { } +// h1.title { } +// p.author { } +// p.date { } nav#toc ol, nav#landmarks ol { padding: 0; margin-left: 1em; } nav#toc ol li, diff --git a/book/epub/sass/theme/fonts.scss b/book/epub/sass/theme/fonts.scss index 173f3f2ee..8a8937453 100644 --- a/book/epub/sass/theme/fonts.scss +++ b/book/epub/sass/theme/fonts.scss @@ -1,70 +1,26 @@ -/* Frankenfont */ -/* A custom font made by combining glyphs from mononoki, DejaVu Sans Mono, */ -/* Symbola and Droid, and adjusting the width where necessary to get a */ -/* consistent fixed-width font. */ +/* JuliaMono */ +/* See: https://juliamono.netlify.app/download/ */ @font-face { - font-family: 'Frankenfont'; - src: url('../fonts/Frankenfont-Regular.ttf') format('ttf'); + font-family: 'JuliaMono'; + src: url('../fonts/JuliaMono-Regular.woff2') format('woff2'); font-weight: normal; font-style: normal; } - -/* DejaVu Sans */ -/* See: https://dejavu-fonts.github.io/ */ @font-face { - font-family: 'DejaVu Sans'; - src: url('../fonts/DejaVuSans-Regular.ttf') format('ttf'); - font-weight: normal; - font-style: normal; -} - -@font-face { - font-family: 'DejaVu Sans'; - src: url('../fonts/DejaVuSans-Bold.ttf') format('ttf'); - font-weight: bold; - font-style: normal; -} - -@font-face { - font-family: 'DejaVu Sans'; - src: url('../fonts/DejaVuSans-Oblique.ttf') format('ttf'); - font-weight: normal; - font-style: oblique; -} - -@font-face { - font-family: 'DejaVu Sans'; - src: url('../fonts/DejaVuSans-BoldOblique.ttf') format('ttf'); - font-weight: bold; - font-style: oblique; -} - -/* DejaVu Serif */ -/* See: https://dejavu-fonts.github.io/ */ -@font-face { - font-family: 'DejaVu Serif'; - src: url('../fonts/DejaVuSerif-Regular.ttf') format('ttf'); - font-weight: normal; - font-style: normal; -} - -@font-face { - font-family: 'DejaVu Serif'; - src: url('../fonts/DejaVuSerif-Bold.ttf') format('ttf'); + font-family: 'JuliaMono'; + src: url('../fonts/JuliaMono-Bold.woff2') format('woff2'); font-weight: bold; font-style: normal; } - @font-face { - font-family: 'DejaVu Serif'; - src: url('../fonts/DejaVuSerif-Italic.ttf') format('ttf'); + font-family: 'JuliaMono'; + src: url('../fonts/JuliaMono-RegularItalic.woff2') format('woff2'); font-weight: normal; font-style: italic; } - @font-face { - font-family: 'DejaVu Serif'; - src: url('../fonts/DejaVuSerif-BoldItalic.ttf') format('ttf'); + font-family: 'JuliaMono'; + src: url('../fonts/JuliaMono-BoldItalic.woff2') format('woff2'); font-weight: bold; font-style: italic; } diff --git a/tools/Buildfile.hs b/tools/Buildfile.hs index a37b9c1d6..e96839cda 100644 --- a/tools/Buildfile.hs +++ b/tools/Buildfile.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + {-# HLINT ignore "Redundant <&>" #-} {-# HLINT ignore "Monad law, left identity" #-} @@ -506,7 +507,7 @@ main = do -- Set writer options epubMetadata <- readFile' (tmpEpubDir "epub-metadata.xml") - epubFonts <- getDirectoryFiles "" [epubFontsDir "*.ttf"] + epubFonts <- getDirectoryFiles "" [epubFontsDir "*.woff2"] epubTemplate <- Pandoc.compileTemplateFile (epubTemplateDir "epub.html") let writerOptsForEpub = @@ -551,12 +552,12 @@ data Project | Course {courseId :: String} deriving (Show, Typeable, Eq, Generic, Hashable, Binary, NFData) -getCourseId :: MonadError String m => FilePath -> m String +getCourseId :: (MonadError String m) => FilePath -> m String getCourseId src | courseDir `List.isPrefixOf` src = return $ makeRelative courseDir (takeDirectory src) | otherwise = throwError $ printf "Courses must be in '%s', '%s':" courseDir src -getProject :: MonadError String m => FilePath -> m Project +getProject :: (MonadError String m) => FilePath -> m Project getProject src | chapterDir `List.isPrefixOf` src = return Main | courseDir `List.isPrefixOf` src = Course <$> getCourseId src @@ -815,7 +816,7 @@ defaultHtmlMinifierArgs = "--remove-style-link-type-attributes" ] -htmlMinifier :: HasCallStack => CmdOutput r -> [CmdOption] -> [String] -> LazyText.Text -> Action r +htmlMinifier :: (HasCallStack) => CmdOutput r -> [CmdOption] -> [String] -> LazyText.Text -> Action r htmlMinifier cmdOutput cmdOpts args stdin = getMode >>= \case Development -> do @@ -967,16 +968,16 @@ pattern AgdaFileInfo -------------------------------------------------------------------------------- -- Helper functions -failOnError :: MonadFail m => Either String a -> m a +failOnError :: (MonadFail m) => Either String a -> m a failOnError = either fail return -failOnNothing :: MonadFail m => String -> Maybe a -> m a +failOnNothing :: (MonadFail m) => String -> Maybe a -> m a failOnNothing msg = maybe (fail msg) return -ignoreError :: Monoid a => Either String a -> a +ignoreError :: (Monoid a) => Either String a -> a ignoreError = fromRight mempty -ignoreNothing :: Monoid a => Maybe a -> a +ignoreNothing :: (Monoid a) => Maybe a -> a ignoreNothing = fromMaybe mempty rightToMaybe :: Either e a -> Maybe a diff --git a/tools/Buildfile/Script.hs b/tools/Buildfile/Script.hs index 1693c219c..e6f59b5b7 100644 --- a/tools/Buildfile/Script.hs +++ b/tools/Buildfile/Script.hs @@ -6,7 +6,8 @@ import Data.Text qualified as Text import Data.Text.Lazy qualified as LazyText import Shoggoth.Configuration (Mode (Development), getMode) import Shoggoth.Prelude (Action, Url, takeBaseName) -import Shoggoth.Routing (RoutingTable, routeUrl) +import Shoggoth.Routing (RoutingTable) +import Shoggoth.Routing qualified as Route (url) data Script = ScriptFile @@ -27,8 +28,8 @@ fromFilePath :: Action Script fromFilePath out = do let id = Text.pack (takeBaseName out) - url <- routeUrl out - (url, integrity) <- (,) <$> routeUrl out <*> ?getDigest out + url <- Route.url out + (url, integrity) <- (,) <$> Route.url out <*> ?getDigest out return $ ScriptFile { scriptId = "script-" <> id, diff --git a/tools/Buildfile/Stylesheet.hs b/tools/Buildfile/Stylesheet.hs index 540d9bcb9..d5b7cfb37 100644 --- a/tools/Buildfile/Stylesheet.hs +++ b/tools/Buildfile/Stylesheet.hs @@ -7,7 +7,8 @@ import Data.Text qualified as Text import Data.Text.Lazy qualified as LazyText import Shoggoth.Configuration (Mode (Development), getMode) import Shoggoth.Prelude (Action, Url, getEnvWithDefault, takeBaseName) -import Shoggoth.Routing (RoutingTable, routeUrl) +import Shoggoth.Routing (RoutingTable) +import Shoggoth.Routing qualified as Route (url) data Stylesheet = Stylesheet { stylesheetTitle :: Text, @@ -29,7 +30,7 @@ fromFilePath :: Action Stylesheet fromFilePath out = do let id = Text.pack (takeBaseName out) - (url, integrity) <- (,) <$> routeUrl out <*> ?getDigest out + (url, integrity) <- (,) <$> Route.url out <*> ?getDigest out return $ Stylesheet { stylesheetTitle = Text.toTitle id, diff --git a/web/assets/fonts/Frankenfont-Regular.woff b/web/assets/fonts/Frankenfont-Regular.woff deleted file mode 100644 index ff42a5ef5..000000000 Binary files a/web/assets/fonts/Frankenfont-Regular.woff and /dev/null differ diff --git a/web/assets/fonts/Frankenfont-Regular.woff2 b/web/assets/fonts/Frankenfont-Regular.woff2 deleted file mode 100644 index 3d121d311..000000000 Binary files a/web/assets/fonts/Frankenfont-Regular.woff2 and /dev/null differ diff --git a/web/assets/fonts/JuliaMono-Bold.woff2 b/web/assets/fonts/JuliaMono-Bold.woff2 new file mode 100644 index 000000000..4c9d30b48 Binary files /dev/null and b/web/assets/fonts/JuliaMono-Bold.woff2 differ diff --git a/web/assets/fonts/JuliaMono-BoldItalic.woff2 b/web/assets/fonts/JuliaMono-BoldItalic.woff2 new file mode 100644 index 000000000..170e8aa0f Binary files /dev/null and b/web/assets/fonts/JuliaMono-BoldItalic.woff2 differ diff --git a/web/assets/fonts/JuliaMono-Regular.woff2 b/web/assets/fonts/JuliaMono-Regular.woff2 new file mode 100644 index 000000000..3a5e27f0b Binary files /dev/null and b/web/assets/fonts/JuliaMono-Regular.woff2 differ diff --git a/web/assets/fonts/JuliaMono-RegularItalic.woff2 b/web/assets/fonts/JuliaMono-RegularItalic.woff2 new file mode 100644 index 000000000..007a2625f Binary files /dev/null and b/web/assets/fonts/JuliaMono-RegularItalic.woff2 differ diff --git a/web/sass/theme/_layout.scss b/web/sass/theme/_layout.scss index da069f50d..de113b535 100644 --- a/web/sass/theme/_layout.scss +++ b/web/sass/theme/_layout.scss @@ -80,10 +80,10 @@ padding: 5px 10px; // Gaps between nav items, but not on the last one + margin-left: 20px; &:not(:last-child) { margin-right: 0; } - margin-left: 20px; } @media screen and (min-width: $on-medium) { @@ -103,11 +103,10 @@ .page-link { display: inline; padding: 0; - + margin-left: auto; &:not(:last-child) { margin-right: 20px; } - margin-left: auto; } } } diff --git a/web/sass/theme/agda-dark.scss b/web/sass/theme/agda-dark.scss index 3eb4c1ea3..695b7b691 100644 --- a/web/sass/theme/agda-dark.scss +++ b/web/sass/theme/agda-dark.scss @@ -1,5 +1,5 @@ @mixin code-font { - font-family: 'Frankenfont', 'FreeMono', 'DejaVu Sans Mono', 'mononoki', 'Source Code Pro', monospace; + font-family: 'JuliaMono'; font-size: .85em; } @mixin code-container { @@ -42,7 +42,7 @@ pre.Spec { .Number { color: #b051eb } .Symbol { color: #8b8b8b } .PrimitiveType { color: #4343ca } -.Operator {} +// .Operator {} /* NameKinds. */ .Bound { color: #bbbbbb } @@ -57,7 +57,7 @@ pre.Spec { .Record { color: #4343ca } /* OtherAspects. */ -.DottedPattern {} +// .DottedPattern {} .UnsolvedMeta { color: #bbbbbb; background: yellow } .UnsolvedConstraint { color: #bbbbbb; background: yellow } .TerminationProblem { color: #bbbbbb; background: #FFA07A } diff --git a/web/sass/theme/agda.scss b/web/sass/theme/agda.scss index c6639f633..c318f1d73 100644 --- a/web/sass/theme/agda.scss +++ b/web/sass/theme/agda.scss @@ -1,5 +1,5 @@ @mixin code-font { - font-family: 'Frankenfont', 'FreeMono', 'DejaVu Sans Mono', 'mononoki', 'Source Code Pro', monospace; + font-family: 'JuliaMono'; font-size: .85em; } @mixin code-container { @@ -42,7 +42,7 @@ pre.Spec { .Number { color: #A020F0 } .Symbol { color: #404040 } .PrimitiveType { color: #0000CD } -.Operator {} +// .Operator {} /* NameKinds. */ .Bound { color: black } @@ -57,7 +57,7 @@ pre.Spec { .Record { color: #0000CD } /* OtherAspects. */ -.DottedPattern {} +// .DottedPattern {} .UnsolvedMeta { color: black; background: yellow } .UnsolvedConstraint { color: black; background: yellow } .TerminationProblem { color: black; background: #FFA07A } diff --git a/web/sass/theme/custom-variables.scss b/web/sass/theme/custom-variables.scss index 2a2d0fa4e..a8b54b3bb 100644 --- a/web/sass/theme/custom-variables.scss +++ b/web/sass/theme/custom-variables.scss @@ -1 +1,2 @@ // Placeholder to allow overriding predefined variables smoothly. +$code-font-family: 'JuliaMono'; diff --git a/web/sass/theme/fonts.scss b/web/sass/theme/fonts.scss index 160d4e454..f392b3289 100644 --- a/web/sass/theme/fonts.scss +++ b/web/sass/theme/fonts.scss @@ -3,12 +3,30 @@ // Symbola and Droid, and adjusting the width where necessary to get a // consistent fixed-width font. @font-face { - font-family: "Frankenfont"; - src: url("../fonts/Frankenfont-Regular.woff2") format("woff2"), - url("../fonts/Frankenfont-Regular.woff") format("woff"); + font-family: 'JuliaMono'; + src: url('../fonts/JuliaMono-Regular.woff2') format('woff2'); font-weight: normal; font-style: normal; } +@font-face { + font-family: 'JuliaMono'; + src: url('../fonts/JuliaMono-Bold.woff2') format('woff2'); + font-weight: bold; + font-style: normal; +} +@font-face { + font-family: 'JuliaMono'; + src: url('../fonts/JuliaMono-RegularItalic.woff2') format('woff2'); + font-weight: normal; + font-style: italic; +} +@font-face { + font-family: 'JuliaMono'; + src: url('../fonts/JuliaMono-BoldItalic.woff2') format('woff2'); + font-weight: bold; + font-style: italic; +} + @import "fontawesome/fontawesome",