From f9b5a2903a5c53c3aa2bb3083012d65b88ff487e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 15 Sep 2023 00:39:28 +0200 Subject: [PATCH] fix: header-data.bmp --- DocGen4/Output/ToJson.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean index 4d87394..ee3ae3c 100644 --- a/DocGen4/Output/ToJson.lean +++ b/DocGen4/Output/ToJson.lean @@ -36,7 +36,7 @@ structure JsonModule where deriving FromJson, ToJson structure JsonHeaderIndex where - headers : List (String × String) := [] + declarations : List (String × JsonDeclaration) := [] structure JsonIndexedDeclarationInfo where kind : String @@ -51,7 +51,7 @@ structure JsonIndex where instancesFor : HashMap String (RBTree String Ord.compare) := .empty instance : ToJson JsonHeaderIndex where - toJson idx := Json.mkObj <| idx.headers.map (fun (k, v) => (k, toJson v)) + toJson idx := Json.mkObj <| idx.declarations.map (fun (k, v) => (k, toJson v)) instance : ToJson JsonIndex where toJson idx := Id.run do @@ -70,7 +70,7 @@ instance : ToJson JsonIndex where return finalJson def JsonHeaderIndex.addModule (index : JsonHeaderIndex) (module : JsonModule) : JsonHeaderIndex := - let merge idx decl := { idx with headers := (decl.info.name, decl.header) :: idx.headers } + let merge idx decl := { idx with declarations := (decl.info.name, decl) :: idx.declarations } module.declarations.foldl merge index def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM JsonIndex := do