diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index ab43b0b7..bc1b5ad0 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 e1e89c07..55311419 100644
--- a/src/verso-manual/VersoManual/Html.lean
+++ b/src/verso-manual/VersoManual/Html.lean
@@ -511,12 +511,17 @@ 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:"
+ -- 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
@@ -524,4 +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
- return some <| .tag tag (← attrs.mapM rwAttr) content
+ -- 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 ) 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)
+ 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
+ else attrs
+ let attrs ← attrs.mapM rwAttr
+ return some <| .tag tag attrs content