feat: save section numbers in xref table

src/verso-manual/VersoManual/Basic.lean

@@ -773,6 +773,15 @@ def TraverseState.linkTargets (state : TraverseState) : Code.LinkTargets where
      (state.resolveDomainObject syntaxKindDomain k.toString).toOption) <&>
     fun (path, htmlId) => path.link (some htmlId.toString)
 
+def sectionNumberString (num : Array Numbering) : String := Id.run do
+  let mut out := ""
+  for n in num do
+    out := out ++
+      match n with
+      | .nat n => s!"{n}."
+      | .letter a => s!"{a}."
+  out
+
 
 def sectionDomain := `Verso.Genre.Manual.section
 
@@ -825,7 +834,12 @@ instance : Traverse Manual TraverseM where
               externalTags := st.externalTags.insert id (path, slug)
             }
           meta := {meta with tag := external}
-        let jsonMetadata := Json.arr ((← read).inPart part |>.headers.map (Json.str ·.titleString))
+        let getNum : Numbering → String
+          | .nat n => toString n
+          | .letter a => toString a
+        let jsonMetadata :=
+          Json.arr ((← read).inPart part
+            |>.headers.map (fun h => json%{"title": $h.titleString, "number": $(h.metadata.bind (·.assignedNumber) |>.map getNum)}))
         modify (·.saveDomainObject sectionDomain n id
                  |>.saveDomainObjectData sectionDomain n jsonMetadata)
 
@@ -920,15 +934,6 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
       | panic! s!"Inline {i.name} doesn't support TeX"
     impl go id i.data content
 
-def sectionNumberString (num : Array Numbering) : String := Id.run do
-  let mut out := ""
-  for n in num do
-    out := out ++
-      match n with
-      | .nat n => s!"{n}."
-      | .letter a => s!"{a}."
-  out
-
 def sectionString (ctxt : TraverseContext) : Option String :=
   ctxt.sectionNumber.mapM id |>.map sectionNumberString