chore: Sort the declarations internally already

DocGen4/Output/Module.lean

@@ -103,11 +103,10 @@ def internalNav (members : Array Name) (moduleName : Name) : Html :=
   </nav>
 
 def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
-  let sortedMembers := module.members.qsort (λ l r => l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line)
+  let docInfos ← module.members.mapM docInfoToHtml
-  let docInfos ← sortedMembers.mapM docInfoToHtml
   -- TODO: This is missing imports, imported by
   templateExtends (baseHtmlArray module.name.toString) $ #[
-    internalNav (sortedMembers.map DocInfo.getName) module.name,
+    internalNav (module.members.map DocInfo.getName) module.name,
     Html.element "main" false #[] docInfos
   ]
 

DocGen4/Process.lean

@@ -77,9 +77,27 @@ inductive DocInfo where
 | classInfo (info : ClassInfo) : DocInfo
   deriving Inhabited
 
+namespace DocInfo
+
+def getDeclarationRange : DocInfo → DeclarationRange
+| axiomInfo i => i.declarationRange
+| theoremInfo i => i.declarationRange
+| opaqueInfo i => i.declarationRange
+| definitionInfo i => i.declarationRange
+| instanceInfo i => i.declarationRange
+| inductiveInfo i => i.declarationRange
+| structureInfo i => i.declarationRange
+| classInfo i => i.declarationRange
+
+def lineOrder (l r : DocInfo) : Bool :=
+  l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line
+
+end DocInfo
+
 structure Module where
   name : Name
   doc : Option String
+  -- Sorted according to their line numbers
   members : Array DocInfo
   deriving Inhabited
 
@@ -295,16 +313,6 @@ def getArgs : DocInfo → Array Arg
 | structureInfo i => i.args
 | classInfo i => i.args
 
-def getDeclarationRange : DocInfo → DeclarationRange
-| axiomInfo i => i.declarationRange
-| theoremInfo i => i.declarationRange
-| opaqueInfo i => i.declarationRange
-| definitionInfo i => i.declarationRange
-| instanceInfo i => i.declarationRange
-| inductiveInfo i => i.declarationRange
-| structureInfo i => i.declarationRange
-| classInfo i => i.declarationRange
-
 end DocInfo
 
 structure AnalyzerResult where
@@ -338,6 +346,11 @@ def process : MetaM AnalyzerResult := do
         res := res.insert moduleName {module with members := module.members.push dinfo}
       | none => panic! "impossible"
     | none => ()
+
+  -- This could probably be faster if we did an insertion sort above instead
+  for (moduleName, module) in res.toArray do
+    res := res.insert moduleName {module with members := module.members.qsort DocInfo.lineOrder}
+
   return {
     name2ModIdx := env.const2ModIdx,
     moduleNames := env.header.moduleNames,