Search revamp

src/index.lagda.md

@@ -2,7 +2,7 @@
 module index where
 ```
 
-# 1lab {style="margin-top: 0;"}
+# 1lab
 
 A formalised, cross-linked reference resource for cubical methods in
 Homotopy Type Theory. Unlike the [@HoTT], the 1lab is not a "linear"

support/diagram.tex

@@ -28,7 +28,7 @@
 __PREAMBLE__
 
 \ifdefined\labdark
-\definecolor{diagrambg}{HTML}{282C34}
+\definecolor{diagrambg}{HTML}{23272E}
 \definecolor{diagramfg}{HTML}{ABB2BF}
 
 \definecolor{diagramshaded}{HTML}{2b6253}

support/nix/nixpkgs.nix

@@ -1,7 +1,7 @@
 args: import (builtins.fetchTarball {
   name   = "1lab-nixpkgs";
-  url    = "https://github.com/nixos/nixpkgs/archive/bf39054f8666a98196671269351e42db7e0db6bc.tar.gz";
-  sha256 = "sha256:0f9k3c6qjsn2aw5jhyz8pqs5saajgi4wkrbj0yrsp1k0vpx4yqx6";
+  url    = "https://github.com/nixos/nixpkgs/archive/6cfbf89825dae72c64188bb218fd4ceca1b6a9e3.tar.gz";
+  sha256 = "sha256:17m78fn3y2x44zgdm428k3l6xamyw6vnz2vd68nj5kxlkbfqnynr";
 }) ({
   overlays = [ (import ./haskell-packages.nix) ];
 } // args)

support/shake/app/Main.hs

@@ -162,6 +162,7 @@ rules = do
         , "_build/html/static/search.json"
         , "_build/html/css/default.css"
         , "_build/html/main.js"
+        , "_build/html/start.js"
         , "_build/html/code-only.js"
         ]
 

support/shake/app/Shake/Markdown.hs

@@ -390,8 +390,8 @@ foldEquations _ (to@(TagOpen "a" attrs):tt@(TagText t):tc@(TagClose "a"):rest)
     go href (c:cs) = c:go href cs
     go _ [] = []
 foldEquations False (TagClose "html":cs) =
- [TagOpen "style" [], TagText ".equations { display: none !important; }", TagClose "style", TagClose "html"]
- ++ foldEquations True cs
+  [TagOpen "style" [], TagText ".equations { display: none !important; }", TagClose "style", TagClose "html"]
+  ++ foldEquations True cs
 foldEquations has_eqn (c:cs) = c:foldEquations has_eqn cs
 foldEquations _ [] = []
 
@@ -405,7 +405,6 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) =
     { idIdent = module'
     , idAnchor = module' <> ".html"
     , idType = Nothing
-    , idDesc = stringify <$> (Map.lookup "description" meta <|> Map.lookup "pagetitle" meta)
     , idDefines = Nothing
     }
 
@@ -430,7 +429,6 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) =
         { idIdent  = Text.intercalate " > " . reverse $ map snd path'
         , idAnchor = module' <> ".html#" <> hId
         , idType   = Nothing
-        , idDesc   = getDesc xs
         , idDefines = Text.words <$> lookup "defines" keys
         } <$> go xs
   go (Div (hId, _, keys) blocks:xs) | hId /= "" = do
@@ -440,7 +438,6 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) =
       { idIdent  = Text.intercalate " > " . reverse $ hId:map snd path
       , idAnchor = module' <> ".html#" <> hId
       , idType   = Nothing
-      , idDesc   = getDesc blocks
       , idDefines = (:) hId . Text.words <$> lookup "alias" keys
       } <$> go xs
   go (_:xs) = go xs
@@ -452,14 +449,6 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) =
   write = writePlain def{ writerExtensions = enableExtension Ext_raw_html (writerExtensions def) }
   renderPlain inlines = either (error . show) id . runPure . write $ Pandoc mempty [Plain inlines]
 
-  -- | Attempt to find the "description" of a heading. Effectively, if a header
-  -- is followed by a paragraph, use its contents.
-  getDesc (Para x:_) = Just (renderPlain x)
-  getDesc (Plain x:_) = Just (renderPlain x)
-  getDesc (Div (_, cls, _) _:xs) | "warning" `elem` cls = getDesc xs
-  getDesc (BlockQuote blocks:_) = getDesc blocks
-  getDesc _ = Nothing
-
 htmlInl :: Text -> Inline
 htmlInl = RawInline "html"
 

support/shake/app/Shake/SearchData.hs

@@ -13,7 +13,6 @@ data SearchTerm = SearchTerm
   { idIdent   :: Text
   , idAnchor  :: Text
   , idType    :: Maybe Text
-  , idDesc    :: Maybe Text
   , idDefines :: Maybe [Text]
   }
   deriving (Eq, Show, Ord, Generic, ToJSON, FromJSON)

support/web/css/code.scss

@@ -26,6 +26,7 @@ div.sourceCode {
 div.sourceCode > pre {
   background-color: var(--code-bg);
   color:            var(--code-fg);
+
   flex-grow: 0;
 
   overflow-x: auto;
@@ -122,7 +123,7 @@ a[href].hover-highlight {
   }
 
   // background-color: $code-bg;
-  font-family: 'Julia Mono', 'Iosevka', 'Fantasque Sans Mono', 'Roboto Mono', monospace;
+  @include monospaced;
   font-weight: 400;
 
   font-size: initial;
@@ -158,14 +159,18 @@ code.do, span.do { color: var(--code-string); } /* Documentation */
 code.an, span.an { color: var(--code-string); } /* Annotation */
 code.cv, span.cv { color: var(--code-string); } /* CommentVar */
 
-.typeTooltip {
+.type-tooltip {
   position: absolute;
   z-index: 100;
 
   font-size: 0.8em;
   color: var(--code-fg);
   background: var(--code-bg);
 
-  padding: 0.3em;
+  &.sourceCode {
+    padding: 0.3em;
+    border:  0;
+  };
+
   box-shadow: 2px 2px 6px var(--shadow);
 }