Use JuliaMono as code font (#1034)

* Use JuliaMono as the code font

* Fix code font

* Update README

* [pre-commit.ci] auto fixes from pre-commit.com hooks

for more information, see https://pre-commit.ci

---------

Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com>

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

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        }

book/epub/sass/theme/epub.scss

@@ -1,16 +1,16 @@
 /* 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; }
 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,

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;
 }

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

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,

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,

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;
     }
   }
 }

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        }

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        }

web/sass/theme/custom-variables.scss

@@ -1 +1,2 @@
 // Placeholder to allow overriding predefined variables smoothly.
+$code-font-family: 'JuliaMono';

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",