Fix/relative urls

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 `<base>`-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 `<base>`-relative.
+    -- Also adjusts relative image URLs to account for the <base> 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

src/verso-manual/VersoManual/Html.lean

@@ -511,17 +511,37 @@ 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 <base> 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
     if tag == "base" then return none
     -- 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 <img> tags with relative src paths, prefix with the page path so that
+    -- the URL resolves correctly via the <base> tag.  User-authored image
+    -- references (from Markdown ![alt](path)) produce page-relative URLs, but
+    -- the <base> 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