Skip to content

Commit

Permalink
fix: do not escape module names for html files (#267)
Browse files Browse the repository at this point in the history
This matches how lean file names are not escaped.
  • Loading branch information
eric-wieser authored Feb 26, 2025
1 parent e3f8a87 commit 32578e5
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions DocGen4/Output/Base.lean
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ def templateLiftExtends {α β} {m n} [Bind m] [MonadLiftT n m] (base : α → n
Returns the doc-gen4 link to a module name.
-/
def moduleNameToLink (n : Name) : BaseHtmlM String := do
let parts := n.components.map Name.toString
let parts := n.components.map (Name.toString (escape := False))
return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"

/--
Expand All @@ -178,14 +178,14 @@ def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do
Returns the path to the HTML file that contains information about a module.
-/
def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
let parts := n.components.map Name.toString
let parts := n.components.map (Name.toString (escape := False))
FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"

/--
Returns the directory of the HTML file that contains information about a module.
-/
def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
let parts := n.components.dropLast.map Name.toString
let parts := n.components.dropLast.map (Name.toString (escape := False))
basePath / parts.foldl (· / ·) (FilePath.mk ".")

section Static
Expand Down

0 comments on commit 32578e5

Please sign in to comment.