diff --git a/support/shake/app/Shake/Markdown.hs b/support/shake/app/Shake/Markdown.hs index a0e87f17c..c51c5a82a 100644 --- a/support/shake/app/Shake/Markdown.hs +++ b/support/shake/app/Shake/Markdown.hs @@ -54,10 +54,6 @@ import Shake.Git import HTML.Emit import Definitions -import Control.Exception (evaluate) -import Control.DeepSeq -import Text.Show.Pretty (ppShow) -import Text.Printf readLabMarkdown :: MonadIO m => FilePath -> m Pandoc readLabMarkdown fp = liftIO cont where @@ -200,8 +196,6 @@ buildMarkdown modname input output = do let search = query (getHeaders (Text.pack modname)) markdown (markdown, MarkdownState references dependencies) <- runWriterT (walkM patchBlock markdown) - markdown <- liftIO $ evaluate (let x = walk floatNotes markdown in rnf x `seq` x) - -- error $ ppShow markdown need dependencies baseUrl <- getBaseUrl @@ -287,23 +281,6 @@ patchInline _ (Str s) patchInline _ h = pure h --- | Turn footnotes into sidenotes. -floatNotes :: Pandoc -> Pandoc -floatNotes = flip evalState 0 . walkM \case - Note blk -> do - this <- get - put (this + 1) - let - unwrap (Plain is) = is - unwrap (Para is) = is - unwrap b = error $ "Unsupported block type in footnote: " <> ppShow b - - rendered = either (error . show) id . runPure . writeHtml5String def $ Pandoc mempty [Plain (blk >>= unwrap)] - - ref = " Text.pack (show this) <> "\" />" - pure $ Span ("", ["sidenote"], []) [htmlInl ref, Span ("", ["sidenote-content"], []) [htmlInl rendered]] - x -> pure x - data MarkdownState = MarkdownState { mdReferences :: [Val Text] -- ^ List of references extracted from Pandoc's "reference" div. , mdDependencies :: [String] -- ^ Additional files this markdown file depends on. diff --git a/support/web/css/code.scss b/support/web/css/code.scss index 059b8d62d..546d6d7ae 100644 --- a/support/web/css/code.scss +++ b/support/web/css/code.scss @@ -17,7 +17,6 @@ code, pre, .sourceCode { font-family: 'Julia Mono'; font-size: var(--code-font-size); font-weight: 500; - clear: both; } div.sourceCode { diff --git a/support/web/css/default.scss b/support/web/css/default.scss index 936606558..f0c50cd50 100644 --- a/support/web/css/default.scss +++ b/support/web/css/default.scss @@ -10,24 +10,26 @@ @import "code.scss"; html { - min-height: 100%; height: 100%; - max-width: 100%; margin: 0; background-color: var(--text-bg); color: var(--text-fg); } +html, body, main, div#post-toc-container { + min-height: 100vh; + max-width: 100vw; +} + :root { --serif: "EB Garamond", "Times New Roman", "serif"; --sans-serif: "Inria Sans", -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, Oxygen, Ubuntu, Cantarell, 'Open Sans', 'Helvetica Neue', sans-serif; --font-size: 1.4rem; --code-font-size: calc(0.85 * var(--font-size)); - --content-width: 65%; - --sidenote-width: 25em; - --sidenote-separation: 3em; + --content-width: 50vw; + --sidenote-separation: 2em; &.sans-serif { --serif: ""; @@ -219,56 +221,57 @@ table { } } -span.sidenote { - counter-increment: footnote-counter; +span.sidenote-baseline-mark { + width: 0px; + vertical-align: baseline; + display: inline-block; +} - .sidenote-content { - position: relative; - display: none; +div.sidenote { + position: absolute; + right: 0; - &:before { - display: none; - content: counter(footnote-counter); - font-size: 1.0rem; - position: absolute; - left: -1.5ex; - } - } + :nth-child(2) { margin-block-start: 0; } + :last-child { margin-block-end: 0; } - .sidenote-toggle { display: none; } + font-size: smaller; + line-height: 1.1; - .sidenote-toggle:checked + .sidenote-content { - display: block; - float: left; - clear: both; - margin: 1em 2.5%; - width: 95%; + width: 100%; + text-align: justify; + hyphens: auto; + + > span.sidenote-number { + position: absolute; + top: -1.5em; + + text-align: right; + width: 100%; + + border-bottom: 1px dotted black; } - .sidenote-number { - display: inline-block; + a.footnote-back { display: none; } +} - &:after { - content: counter(footnote-counter); - font-size: 1.0rem; +section.footnotes { + @include widescreen { display: none; } + display: block; +} - // Pretend to be a link - color: var(--primary); - cursor: pointer; - text-decoration: underline; +aside#sidenote-container { + @include widescreen { display: block; } - position: relative; - top: -0.2em; - } - } + display: none; + + position: relative; } -details { - margin-block: 1em; - border-left: 5px solid var(--note-bg); - padding-left: 1rem; +// @include widescreen { aside#sidenote-container { display: block; } } - @include contains-code(); +details { + @include left-bordered(var(--note-bg)); + // @include contains-code(); > summary { list-style-type: none; @@ -434,7 +437,7 @@ div.diagram-container { } } -article a[href], div#return > a[href], div#top > a[href], aside#toc > div#toc-container ul a[href] { +main a[href], div#return > a[href], div#top > a[href], aside#toc > div#toc-container ul a[href] { color: var(--primary); text-decoration: none; &:hover { @@ -562,7 +565,7 @@ input { } } -@media only screen and (min-width: 95rem) { +@include widescreen { .narrow-only { display: none !important; } @@ -573,10 +576,14 @@ input { div#post-toc-container { display: grid; - // The 0 minimum is required to avoid overflow, see https://css-tricks.com/preventing-a-grid-blowout/ - grid-template-columns: 1fr minmax(0, 5fr); + grid-template-areas: ". sidebar . content gutter ."; + + // The 0 minimum is required to avoid overflow, see + // https://css-tricks.com/preventing-a-grid-blowout/ + grid-template-columns: 0.1fr 1fr 0.1fr minmax(0, 3fr) 1fr 0.2fr; aside#toc { + grid-column: sidebar; h3 { @include centered-contents; } font-family: var(--sans-serif); @@ -587,17 +594,15 @@ input { box-sizing: border-box; top: $page-padding; - bottom: $page-padding; - max-height: 90vh; + height: calc(100vh - (2 * #{$page-padding})); display: flex; flex-direction: column; gap: 0.5rem; width: 100%; - margin-right: 1rem; - padding-right: 1rem; + z-index: 1; div#toc-container { box-sizing: border-box; @@ -657,13 +662,13 @@ input { } } - article > { - :not(pre, div.sourceCode) { - width: var(--content-width); - } - ul, ol, dl, details { - box-sizing: border-box; - } + article { + grid-column: content; + } + + aside#sidenote-container { + grid-column: gutter; + margin-left: calc(var(--sidenote-separation)); } } @@ -672,35 +677,5 @@ input { grid-template-columns: 1fr 1fr; gap: 1em; } - - padding: 0; - padding-bottom: 0.4em; - } - - span.sidenote { - .sidenote-content:before { - display: revert; - } - - .sidenote-number:after { - color: var(--text-color); - cursor: text; - text-decoration: none; - } - - .sidenote-toggle:checked + .sidenote-content, .sidenote-toggle:not(:checked) + .sidenote-content { - display: block; - - float: right; - clear: right; - - // margin-right: -45%; - // transform: translateX(120%); - margin-right: calc(-1 * (var(--sidenote-width) + var(--sidenote-separation))); - width: var(--sidenote-width); - - text-align: justify; - hyphens: auto; - } } } diff --git a/support/web/css/mixins.scss b/support/web/css/mixins.scss index 66d229d57..ee4dcc757 100644 --- a/support/web/css/mixins.scss +++ b/support/web/css/mixins.scss @@ -1,7 +1,20 @@ +@mixin left-bordered($bg) { + position: relative; + + &:before { + content: " "; + background-color: $bg; + + height: 100%; + width: 5px; + + position: absolute; + left: calc(-1em - 5px); + } +} + @mixin material($bg) { - border-left: 5px solid $bg; - padding-left: 1rem; - padding-bottom: 0.3em; + @include left-bordered($bg); box-sizing: border-box; >:nth-child(2) { margin-block-start: 0; } @@ -24,13 +37,8 @@ } } - div.#{$name} { + div.#{$name}, details.#{$name} { @include material($bg); - @include contains-code(); - } - - details.#{$name} { - border-left: 5px solid $bg; } } @@ -40,16 +48,13 @@ align-items: center; } -@mixin contains-code { - pre.Agda, div.sourceCode { - /* Undo the indentation so that code stays aligned. */ - padding-left: 0; - border-left: 0; - margin-left: 0; - } -} - @mixin monospaced { font-family: 'Julia Mono', 'Iosevka', 'Fantasque Sans Mono', 'Roboto Mono', monospace; font-weight: 400; } + +@mixin widescreen { + @media only screen and (min-width: $desktop-layout-width) { + @content; + } +} diff --git a/support/web/css/vars.scss b/support/web/css/vars.scss index a27f81d60..e2dd13ed8 100644 --- a/support/web/css/vars.scss +++ b/support/web/css/vars.scss @@ -105,3 +105,6 @@ $light-button-hover-bg: $zinc-200; $dark-text-bg: #23272E; $dark-text-fg: #ABB2BF; + +// "Desktop layout": navigation bar, content, sidenotes. +$desktop-layout-width: 110rem; diff --git a/support/web/js/depgraph.tsx b/support/web/js/depgraph.tsx index 1701d47b2..9b6fe2a55 100644 --- a/support/web/js/depgraph.tsx +++ b/support/web/js/depgraph.tsx @@ -431,9 +431,7 @@ document.addEventListener('DOMContentLoaded', async () => { addExpand = () => { ruler.style.display = "block"; - const expand = + const expand = ; expand.addEventListener("click", () => { ruler.style.display = "none"; @@ -443,7 +441,7 @@ document.addEventListener('DOMContentLoaded', async () => { }); reset(); - container.appendChild(expand); + container.appendChild(
{expand}
); }; addExpand(); diff --git a/support/web/js/equations.ts b/support/web/js/equations.ts index 420b2a95a..7aa52a5ba 100644 --- a/support/web/js/equations.ts +++ b/support/web/js/equations.ts @@ -1,5 +1,30 @@ import { equationSetting, hiddenCodeSetting, serifFontSetting } from "./lib/settings"; +export function scrollToHash() { + if (window.location.hash === '') return; + + const + id = window.location.hash.slice(1), + // #id doesn't work with numerical IDs + elem = document.querySelector(`[id="${id}"]`); + + if (!(elem instanceof HTMLElement)) return; + + // If the element is in a commented-out block or a
tag, unhide it + // and scroll to it. + const commentedOut = elem.closest('.commented-out') as HTMLElement | null; + + if (commentedOut) + commentedOut.style.display = 'revert'; + + const details = elem.closest('details') as HTMLElement | null; + if (details) + details.setAttribute("open", ""); + + if (commentedOut || details) + elem.scrollIntoView(); +} + window.addEventListener("DOMContentLoaded", () => { /* I tried really hard to do this with only CSS but :first-of-type is @@ -61,23 +86,4 @@ window.addEventListener("DOMContentLoaded", () => { window.addEventListener("hashchange", scrollToHash); -function scrollToHash() { - if (window.location.hash === '') return; - - const id = window.location.hash.slice(1); - // #id doesn't work with numerical IDs - const elem = document.querySelector(`[id="${id}"]`); - if (!(elem instanceof HTMLElement)) return; - // If the element is in a commented-out block or a
tag, unhide it - // and scroll to it. - const commentedOut = elem.closest('.commented-out') as HTMLElement | null; - if (commentedOut) - commentedOut.style.display = 'revert'; - const details = elem.closest('details') as HTMLElement | null; - if (details) - details.setAttribute("open", ""); - if (commentedOut || details) - elem.scrollIntoView(); -} - export { }; diff --git a/support/web/js/highlight-hover.ts b/support/web/js/highlight-hover.ts index 59012dd62..1a2ede4dc 100644 --- a/support/web/js/highlight-hover.ts +++ b/support/web/js/highlight-hover.ts @@ -64,7 +64,7 @@ document.addEventListener('highlight', (({ detail: { link, on } }: CustomEvent) }); }) as EventListener); -document.addEventListener("DOMContentLoaded", async () => { +export function refreshLinks() { links = Array.from(document.getElementsByTagName("a")); links.forEach(link => { if (link.hasAttribute("href")) { @@ -72,6 +72,8 @@ document.addEventListener("DOMContentLoaded", async () => { link.onmouseout = () => document.dispatchEvent(new CustomEvent('highlight', { detail: { link, on: false } })) } }); -}); +} + +document.addEventListener("DOMContentLoaded", refreshLinks); export {}; diff --git a/support/web/js/lib/jsx.ts b/support/web/js/lib/jsx.ts index 947b7fb48..d213bc9e1 100644 --- a/support/web/js/lib/jsx.ts +++ b/support/web/js/lib/jsx.ts @@ -1,7 +1,7 @@ -export type Content = HTMLElement | string | Content[] | undefined; +export type Content = HTMLElement | string | number | Content[] | undefined; const add = (element: Node, child: Content) => { - if (typeof child === "string") { + if (typeof child === "string" || typeof child === "number") { element.appendChild(document.createTextNode(child.toString())); } else if (child instanceof Array) { child.forEach((x) => add(element, x)); diff --git a/support/web/js/main.ts b/support/web/js/main.ts index 331ccae6e..c39cb8771 100644 --- a/support/web/js/main.ts +++ b/support/web/js/main.ts @@ -5,3 +5,4 @@ import "./search"; import "./sidebar"; import "./prompt"; import "./theme"; +import "./sidenotes"; diff --git a/support/web/js/sidenotes.tsx b/support/web/js/sidenotes.tsx new file mode 100644 index 000000000..951e2532b --- /dev/null +++ b/support/web/js/sidenotes.tsx @@ -0,0 +1,192 @@ +import { refreshLinks } from './highlight-hover'; +import { JSX } from './lib/jsx'; +import { justifiedSetting, serifFontSetting } from './lib/settings'; + +interface Sidenote { + // The actual sidenote element + content: HTMLDivElement; + + // Pair of elements for measuring baseline skip in the sidenote + // context + highMark: Element; + lowMark: Element; + + // Element with which we should align the baseline + target: Element; + + // Enclosing details element, if one exists + blocker?: HTMLDetailsElement; + + // Last vertical position, if one exists + lastTop?: number; +}; + +function getSidenotes(): Sidenote[] { + const notes: Sidenote[] = []; + + document.querySelectorAll("a.footnote-ref[href]").forEach((ref) => { + if (!(ref instanceof HTMLAnchorElement)) return; + const id = Number.parseInt(ref.hash.slice(3)); + if (isNaN(id)) return; + + const parent = document.getElementById(ref.hash.slice(1)); + if (!(parent instanceof HTMLLIElement)) return; + + const + content =
as HTMLDivElement, + lowMark = , + highMark = {lowMark}{id}, + children = Array.from(parent.children).map(e => e.cloneNode(true)); + + children.unshift(highMark); + content.replaceChildren(...children); + + let + blocker: HTMLDetailsElement | undefined = ref.closest("details") ?? undefined, + summary = ref.closest("summary"); + + const target = ; + ref.insertAdjacentElement('afterbegin', target); + + if (summary) { blocker = undefined; } + if (blocker && !blocker.open) { content.style.display = 'none'; } + + notes.push({ content, highMark, lowMark, target, blocker }); + }); + + return notes; +} + +document.addEventListener("DOMContentLoaded", () => { + const parent = document.getElementById("sidenote-container"); + if (!(parent instanceof HTMLElement)) return; + + const notes = getSidenotes(); + console.log(notes); + + parent.replaceChildren(...notes.map(n => n.content)); + refreshLinks(); + + let shown = false; + + const reposition = () => { + if (notes.length < 1) return; + + console.log(`Repositioning ${notes.length} sidenotes`); + + // Start of the next free space to put a sidenote into. + let nextFree = -1; + + // Since everything is done based on screen coordinates, we need to + // know how far off the viewport the top of the sidenote container + // is. + const offset = parent.getBoundingClientRect().top; + + notes.forEach(note => { + const { content, highMark, lowMark, target, blocker, lastTop } = note; + + // If the note is in a
and that
is closed, + // skip laying out the note, and make sure to hide it. + if (blocker && !blocker.open) { + content.style.display = 'none'; + return; + } else if (blocker) { + content.style.display = 'block'; + } + + // Aligning the side notes is very finnicky, at least when there's + // enough space. + // + // The typographically sound way to do this is to align the + // *baselines* of the line containing the reference and the first + // line of the sidenote. Problem: There is no easy way to get the + // text baseline of an element. + // + // The solution: fiddling with numbers. We store + // + // * tgtBaseline - the vertical position of the baseline we want + // to align to + // * noteLineTop - the top position of a line in the sidenote text + // * noteLineBase - the baseline of that same line. + // + // From this, we can calculate noteLineSkip, which measures how + // much vertical space is between the stop of a and the + // baseline of the text contained in that span. + // Starting at the tgtBaseLine and moving *up* noteLineBase px, we + // can calculate precisely *where the sidenote should start* to + // align the baselines. + + const + tgtBaseline = target.getBoundingClientRect().top, + + noteLineTop = highMark.getBoundingClientRect().top, + noteLineBase = lowMark.getBoundingClientRect().top, + + // The baseline is *further* in the page so it is *greater* than + // the top of the line. + noteLineSkip = noteLineBase - noteLineTop, + + // However, it might be the case that there's already a note + // where we want. The positioning in that case is very simple: + // we take whatever is furthest down of [the position we + // calculated] and [the line after the previous note]. + + wanted = tgtBaseline - noteLineSkip - offset, + actual = Math.max(wanted, nextFree); + + if (lastTop != actual) { + note.lastTop = actual; + content.style.top = `${actual}px`; + } + + const height = content.getBoundingClientRect().height; + nextFree = actual + height + noteLineSkip * 1.5; + }); + + // The sidenote container is specified as visibility: hidden in the + // template. This is so we can reposition the reposition the + // sidenotes without them flashing onto the screen in the top-right + // corner on the first frame. The first time we do a reflow, we + // display the container. + if (!shown) { + shown = true; + parent.style.visibility = 'visible'; + } + } + + // We can check whether the page is too narrow to contain the + // sidenotes by checking whether the sidenote-container has a width. + // If the page is too narrow, the sidenotes will get disappeared at + // the CSS level, so doing the reflows wouldn't be an *issue*; it + // would just be wasteful. + const isNarrow = () => { + return parent.getBoundingClientRect().width == 0; + } + + const reflow = () => { + if (!isNarrow()) window.requestAnimationFrame(reposition); + }; + + // Wait for the fonts to finish loading before doing the first reflow. + // + // This means that, on a slower connection (and fresh cache), the + // sidenotes will pop in *after* the page has been laid out the first + // time (with the incorrect font). The alternative is reflowing + // *before* we know the final font metrics, in which case the + // sidenotes will have to wiggle slightly to get into position. + document.fonts.addEventListener("loadingdone", () => { + reflow(); + + window.addEventListener("resize", reflow); + + // Reflowing the entire sidenote container when a
opens is a + // *slight* over-approximation (ha), but it does work. + document.querySelectorAll("details").forEach(d => + d.addEventListener("toggle", reflow)); + + // Make sure that our layout-affecting settings cause the sidenotes + // to be reflowed. + serifFontSetting.onChange(reflow); + justifiedSetting.onChange(reflow); + }); +}); diff --git a/support/web/template.html b/support/web/template.html index 4f8ac36d7..ee8c47131 100644 --- a/support/web/template.html +++ b/support/web/template.html @@ -62,7 +62,7 @@
-
+
- $body$ +$body$ + $if(reference)$
@@ -151,6 +152,10 @@

References

$endif$ + +