From eadb1fdea4a43df281d40ddfe240931245f5526d Mon Sep 17 00:00:00 2001 From: Nicolas Rouquette Date: Sat, 11 Apr 2026 17:36:33 -0700 Subject: [PATCH 1/2] fix: prefix relative image URLs with page path in multi-page HTML Markdown image references like ![alt](graphs/foo.svg) produce in the HTML output. In multi-page mode, the tag causes the browser to resolve these relative URLs from the site root instead of the page's directory, resulting in broken image links. Fix: - Html.relativize now detects tags with relative src attributes and prefixes them with the current page path - relativizeLinks accepts the page Path instead of hardcoding #[] - All three call sites pass the actual page path --- src/verso-manual/VersoManual.lean | 13 +++++++------ src/verso-manual/VersoManual/Html.lean | 20 +++++++++++++++++++- 2 files changed, 26 insertions(+), 7 deletions(-) diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index ab43b0b7d..bc1b5ad00 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -508,9 +508,10 @@ def page (toc : List Html.Toc) (extraHead := config.extraHead) (extraContents := config.extraContents) -def relativizeLinks (html : Html) : Html := - -- Make all absolute URLS be relative to the site root, because that'll make them ``-relative - Html.relativize #[] html +def relativizeLinks (path : Path) (html : Html) : Html := + -- Make all absolute URLS be relative to the site root, because that'll make them ``-relative. + -- Also adjusts relative image URLs to account for the tag. + Html.relativize path html open Output.Html in def xref (toc : List Html.Toc) (xrefJson : String) (findJs : String) (state : TraverseState) (config : Config) : Html := @@ -534,7 +535,7 @@ def emitXrefsJson (dir : System.FilePath) (state : TraverseState) : IO Unit := d def emitFindHtml (toc : List Html.Toc) (dir : System.FilePath) (state : TraverseState) (xrefJson : String) (config : Config) : IO Unit := do emitXrefsJson dir state ensureDir (dir / "find") - IO.FS.writeFile (dir / "find" / "index.html") (Html.doctype ++ (relativizeLinks <| xref toc xrefJson find.js state config).asString) + IO.FS.writeFile (dir / "find" / "index.html") (Html.doctype ++ (relativizeLinks #["find"] <| xref toc xrefJson find.js state config).asString) section @@ -698,7 +699,7 @@ where if config.verbose then IO.println s!"Saving {dir.join "index.html"}" h.putStrLn Html.doctype - h.putStrLn <| Html.asString <| relativizeLinks <| + h.putStrLn <| Html.asString <| relativizeLinks ctxt.path <| page toc ctxt.path text.titleString titleToShow pageContent state config.toConfig thisPageToc (showNavButtons := false) @@ -816,7 +817,7 @@ where if config.verbose then IO.println s!"Saving {dir.join "index.html"}" h.putStrLn Html.doctype - h.putStrLn <| Html.asString <| relativizeLinks <| + h.putStrLn <| Html.asString <| relativizeLinks ctxt.path <| page bookContents ctxt.path part.titleString bookTitle pageContent state config.toConfig thisPageToc if depth > 0 ∧ part.htmlSplit != .never then for p in part.subParts do diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean index e1e89c077..aecd111df 100644 --- a/src/verso-manual/VersoManual/Html.lean +++ b/src/verso-manual/VersoManual/Html.lean @@ -511,6 +511,11 @@ public def relativize (path : Path) (html : Html) : Html := html.visitM (m := ReaderT Path Id) (tag := rwTag) |>.run path where urlAttr (name : String) : Bool := name ∈ ["href", "src", "data", "poster"] + isRelativeContentUrl (url : String) : Bool := + !"/".isPrefixOf url && + !url.startsWith "http://" && !url.startsWith "https://" && + !url.startsWith "data:" && !url.startsWith "mailto:" && + !url.startsWith "#" && !url.startsWith "javascript:" rwAttr (attr : String × String) : ReaderT Path Id (String × String) := do if urlAttr attr.fst && "/".isPrefixOf attr.snd then let path := (← read) @@ -524,4 +529,17 @@ where -- Don't rewrite URLs that come from remote content. This attribute is inserted by the `ref` -- role when referring to remote content. if attrs.any (·.1 == "data-verso-remote") then return none - return some <| .tag tag (← attrs.mapM rwAttr) content + let attrs ← attrs.mapM rwAttr + -- For tags with relative src paths, prefix with the page path so that + -- the URL resolves correctly via the tag. User-authored image + -- references (from Markdown ![alt](path)) produce page-relative URLs, but + -- the tag makes the browser resolve them from the site root. + let path := (← read) + if tag == "img" && path.size > 0 then + let attrs := attrs.map fun attr => + if attr.fst == "src" && isRelativeContentUrl attr.snd then + let pathPrefix := String.join (path.toList.map (· ++ "/")) + { attr with snd := pathPrefix ++ attr.snd } + else attr + return some <| .tag tag attrs content + return some <| .tag tag attrs content From 4ef614206edb6ba7b33e528a0f0b8019ff5b699e Mon Sep 17 00:00:00 2001 From: Nicolas Rouquette Date: Sat, 11 Apr 2026 18:29:24 -0700 Subject: [PATCH 2/2] Simplifies URL rewriting by dropping absolute path conversion Replaces complex path relativization logic with simple leading slash removal for absolute URLs. Since the base tag already points to the site root, root-relative paths resolve correctly without needing traversal sequences. Reorders attribute processing to handle image source prefixing before general URL rewriting. This ensures originally-relative paths can still be distinguished from originally-absolute paths, allowing correct prefixing of user-authored image references. --- src/verso-manual/VersoManual/Html.lean | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean index aecd111df..553114194 100644 --- a/src/verso-manual/VersoManual/Html.lean +++ b/src/verso-manual/VersoManual/Html.lean @@ -516,12 +516,12 @@ where !url.startsWith "http://" && !url.startsWith "https://" && !url.startsWith "data:" && !url.startsWith "mailto:" && !url.startsWith "#" && !url.startsWith "javascript:" + -- Convert absolute URLs to root-relative by stripping the leading `/`. + -- The tag already points to the site root, so root-relative paths + -- resolve correctly without needing `../` sequences. rwAttr (attr : String × String) : ReaderT Path Id (String × String) := do if urlAttr attr.fst && "/".isPrefixOf attr.snd then - let path := (← read) - pure { attr with - snd := path.relativize attr.snd - } + pure { attr with snd := (attr.snd.drop 1).toString } else pure attr rwTag (tag : String) (attrs : Array (String × String)) (content : Html) : ReaderT Path Id (Option Html) := do @@ -529,17 +529,19 @@ where -- Don't rewrite URLs that come from remote content. This attribute is inserted by the `ref` -- role when referring to remote content. if attrs.any (·.1 == "data-verso-remote") then return none - let attrs ← attrs.mapM rwAttr -- For tags with relative src paths, prefix with the page path so that -- the URL resolves correctly via the tag. User-authored image -- references (from Markdown ![alt](path)) produce page-relative URLs, but -- the tag makes the browser resolve them from the site root. + -- This must run BEFORE rwAttr so we can still distinguish originally-relative + -- paths (which need prefixing) from originally-absolute paths (which don't). let path := (← read) - if tag == "img" && path.size > 0 then - let attrs := attrs.map fun attr => + let attrs := if tag == "img" && path.size > 0 then + attrs.map fun attr => if attr.fst == "src" && isRelativeContentUrl attr.snd then let pathPrefix := String.join (path.toList.map (· ++ "/")) { attr with snd := pathPrefix ++ attr.snd } else attr - return some <| .tag tag attrs content + else attrs + let attrs ← attrs.mapM rwAttr return some <| .tag tag attrs content