From 12fe918b2d1f6e6ddd6dc84e693edcf195cf2469 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 21:53:03 +0200 Subject: [PATCH] doc: Output.Template --- DocGen4/Output/Template.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 33d7c59..bc1b216 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -11,7 +11,10 @@ namespace Output open scoped DocGen4.Jsx -def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do +/-- +The HTML template used for all pages. +-/ +def baseHtmlGenerator (title : String) (site : Array Html) : HtmlM Html := do pure @@ -60,8 +63,10 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do - -def baseHtml (title : String) (site : Html) : HtmlM Html := baseHtmlArray title #[site] +/-- +A comfortability wrapper around `baseHtmlGenerator`. +-/ +def baseHtml (title : String) (site : Html) : HtmlM Html := baseHtmlGenerator title #[site] end Output end DocGen4