r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix: header-data.bmp

main
Henrik Böving 2023-09-15 00:39:28 +02:00
parent f7307953d8
commit f9b5a2903a
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
DocGen4/Output/ToJson.lean
View File

@ -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