From 1f9f081c4f869e69cc9ff052d021186accb4fc3c Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sat, 27 Dec 2025 19:25:46 -0500
Subject: [PATCH 1/5] refactor: emit part structure as a string

---
 src/tests/Tests/Basic.lean                    |   1 -
 .../VersoLiterate/Exported.lean               |   2 +-
 src/verso/Verso/Doc.lean                      |  59 +--------
 src/verso/Verso/Doc/ArgParse.lean             |   2 +-
 src/verso/Verso/Doc/Elab/Basic.lean           |   8 +-
 src/verso/Verso/Doc/Elab/Monad.lean           |  16 ++-
 src/verso/Verso/Finished.lean                 |  84 +++++++++++++
 src/verso/Verso/VersoDoc.lean                 | 114 ++++++++++++++++++
 8 files changed, 217 insertions(+), 69 deletions(-)
 create mode 100644 src/verso/Verso/Finished.lean
 create mode 100644 src/verso/Verso/VersoDoc.lean

diff --git a/src/tests/Tests/Basic.lean b/src/tests/Tests/Basic.lean
index 597aef80..7d60c110 100644
--- a/src/tests/Tests/Basic.lean
+++ b/src/tests/Tests/Basic.lean
@@ -276,4 +276,3 @@ info: Verso.Doc.Part.mk
 #### Sub^3section
 
 :::::::
-
diff --git a/src/verso-literate/VersoLiterate/Exported.lean b/src/verso-literate/VersoLiterate/Exported.lean
index 7834a3c0..35bab2ff 100644
--- a/src/verso-literate/VersoLiterate/Exported.lean
+++ b/src/verso-literate/VersoLiterate/Exported.lean
@@ -305,7 +305,7 @@ partial def modToPage [LoadLiterate g] (mod : LitMod) (title : Array (Inline g))
     let p' := stack.back
     stack := stack.pop
     p := pushPart p' p
-  return VersoDoc.mk (fun _ => p) "{}"
+  return VersoDoc.literal p
 where
   docstringBlock (doc : LitVersoDocString) : Array (Block g) :=
     let parts := doc.subsections.map loadPart
diff --git a/src/verso/Verso/Doc.lean b/src/verso/Verso/Doc.lean
index df05f6b4..f494c146 100644
--- a/src/verso/Verso/Doc.lean
+++ b/src/verso/Verso/Doc.lean
@@ -6,19 +6,11 @@ Author: David Thrane Christiansen
 module
 public import Lean.Data.Json
 public import Lean.DocString.Types
-public import SubVerso.Highlighting
 import Verso.Doc.Name
 
 set_option doc.verso true
 set_option pp.rawOnError true
 
-/--
-Identify function; this is a temporary compatibility shim to introduce a new type,
-VersoDoc, that will have a nontrival toPart method.
--/
-@[deprecated "remove or use VersoDoc.toPart" (since := "2025-11-01")]
-public def Lean.Doc.Part.toPart (p : Lean.Doc.Part i b p) := p
-
 namespace Verso
 
 namespace Doc
@@ -62,6 +54,7 @@ public structure Genre : Type 1 where
   The mutable state used in the genre's traversal pass.
   -/
   TraverseState : Type
+deriving Inhabited
 
 @[expose]
 public def Genre.none : Genre := ⟨Empty, Empty, Empty, Unit, Unit⟩
@@ -659,56 +652,6 @@ private partial def Part.reprPrec [Repr genre.Inline] [Repr genre.Block] [Repr g
 public instance [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] : Repr (Part g) where
   reprPrec := private Part.reprPrec
 
-public structure DocReconstruction where
-  highlightDeduplication : SubVerso.Highlighting.Export
-
-
-/--
-The result type of values created by Verso's {lit}`#doc` and {lit}`#docs` commands. A value of type
-{lean}`VersoDoc` represents a not-fully-evaluated document of type {lean}`Part` that can be turned
-into a value by invoking the `VersoDoc.toPart` method. The actual structure of a {lean}`VersoDoc`
-should not be relied on.
--/
-public structure VersoDoc (genre : Genre) where
-  construct : DocReconstruction → Part genre
-
-  /-- Serialization of the DocReconstruction data structure -/
-  docReconstructionData : String := "{}"
-
-instance : Inhabited (VersoDoc genre) where
-  default := VersoDoc.mk (fun _ => Inhabited.default) "{}"
-
-
-/--
-A {lean}`VersoDoc` represents a potentially-not-fully-evaluated {lean}`Part`. Calling {lean}`VersoDoc.toPart` forces
-evaluation of the {lean}`VersoDoc` to a {lean}`Part`.
--/
-public def VersoDoc.toPart: VersoDoc genre → Part genre
-  | .mk construct highlight =>
-    match Json.parse highlight with
-    | .error e => panic! s!"Failed to parse VersoDoc's Export data as JSON: {e}"
-    | .ok json =>
-      if let .ok highlightJson := json.getObjVal? "highlight" then
-        match SubVerso.Highlighting.Export.fromJson? highlightJson with
-        | .error e => panic! s!"Failed to deserialize Export data from parsed JSON: {e}"
-        | .ok table => construct ⟨table⟩
-      else construct ⟨{}⟩
-
-/--
-Replace the metadata in a VersoDoc.
-
-This is something of a hack used as a workaround in LiterateModuleDocs.
--/
-public def VersoDoc.withMetadata (metadata? : Option genre.PartMetadata)  : VersoDoc genre → VersoDoc genre
-  | .mk construct docReconstStr => .mk (fun docReconst => { construct docReconst with metadata := metadata? }) docReconstStr
-
-/--
-Identify function; this is a temporary compatibility shim to introduce a new type,
-VersoDoc, that will have a nontrival toPart method.
--/
-@[deprecated "remove or use VersoDoc.toPart" (since := "2025-11-01")]
-public def Part.toPart (p : Part genre) := p
-
 /--
 Specifies how to modify the context while traversing the contents of a given part.
 -/
diff --git a/src/verso/Verso/Doc/ArgParse.lean b/src/verso/Verso/Doc/ArgParse.lean
index 30b952bf..dc308127 100644
--- a/src/verso/Verso/Doc/ArgParse.lean
+++ b/src/verso/Verso/Doc/ArgParse.lean
@@ -9,7 +9,7 @@ public import Verso.Hover
 import Verso.Parser
 public import Verso.SyntaxUtils
 import Lean.Parser
-import Lean.Elab.GuardMsgs
+public import Lean.Elab.GuardMsgs
 public import Lean.Elab.InfoTree.Types
 public import Lean.ResolveName
 public import Lean.Elab.Term
diff --git a/src/verso/Verso/Doc/Elab/Basic.lean b/src/verso/Verso/Doc/Elab/Basic.lean
index 4fe20620..f4b88771 100644
--- a/src/verso/Verso/Doc/Elab/Basic.lean
+++ b/src/verso/Verso/Doc/Elab/Basic.lean
@@ -5,6 +5,8 @@ Author: David Thrane Christiansen, Rob Simmons
 -/
 module
 public import Verso.Doc
+import Verso.VersoDoc
+public import Verso.Finished
 
 open Lean
 
@@ -19,12 +21,6 @@ public inductive TOC where
   | included (name : Ident)
 deriving Repr, TypeName, Inhabited
 
-public inductive FinishedPart where
-  | mk (titleSyntax : Syntax) (expandedTitle : Array (TSyntax `term)) (titlePreview : String) (metadata : Option (TSyntax `term)) (blocks : Array (TSyntax `term)) (subParts : Array FinishedPart) (endPos : String.Pos.Raw)
-    /-- A name representing a value of type {lean}`VersoDoc` -/
-  | included (name : Ident)
-deriving Repr, BEq
-
 /--
 From a finished part, constructs syntax that denotes its {lean}`Part` value.
 -/
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index 831645e7..5e99fea7 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -21,6 +21,8 @@ public import Verso.Doc.Elab.Basic
 import Verso.Doc.Elab.ExpanderAttribute
 public import Verso.Doc.Name
 import Verso.Doc.DocName
+public import Verso.VersoDoc
+public import Verso.Instances
 
 set_option doc.verso true
 
@@ -462,6 +464,14 @@ unsafe def inlineExpandersForUnsafe (x : Name) : DocElabM (Array InlineExpander)
 @[implemented_by inlineExpandersForUnsafe]
 public opaque inlineExpandersFor (x : Name) : DocElabM (Array InlineExpander)
 
+public def quoteSerializableAux [Monad m] [MonadQuotation m]
+    (aux : Doc.Elab.SerializableAux)
+    : m Term := do
+  let sortedDocs := aux.docs.toArray.qsort (lt := Name.quickLt)
+  let quotedDocs ← sortedDocs.mapM (fun name => ``(Prod.mk $(quote name) (VersoDoc.toPart $(mkIdent name))))
+  ``(Doc.DeserializeAux.mk #[$aux.inlines,*] #[$aux.blocks,*] #[$aux.partMetadata,*] #[$quotedDocs,*])
+
+
 /--
 Creates a term denoting a {lean}`VersoDoc` value from a {lean}`FinishedPart`. This is the final step
 in turning a parsed verso doc into syntax.
@@ -524,7 +534,9 @@ public def FinishedPart.toVersoDoc
         withOptions (·.setBool `compiler.extract_closed false) <| addAndCompile decl
 
   -- Generate and return outermost syntax
-  let finishedSyntax ← finished.toSyntax genreSyntax
+  let (partJson, aux) ← StateT.run finished.serialize {}
+  let quotedAux ← quoteSerializableAux aux
+
   let .some docReconstructionPlaceholder := ctx.docReconstructionPlaceholder
     | throwError "No doc reconstruction placeholder available"
 
@@ -532,7 +544,7 @@ public def FinishedPart.toVersoDoc
     | .none => Json.mkObj []
     | .some table => Json.mkObj [("highlight", table.toExport.toJson)]
 
-  ``(VersoDoc.mk (fun $docReconstructionPlaceholder => $finishedSyntax) $(quote reconstJson.compress))
+  ``(VersoDoc.serialized (fun $docReconstructionPlaceholder => $quotedAux) $(quote partJson.compress) $(quote reconstJson.compress) none)
 
 
 public abbrev BlockExpander := Syntax → DocElabM (TSyntax `term)
diff --git a/src/verso/Verso/Finished.lean b/src/verso/Verso/Finished.lean
new file mode 100644
index 00000000..c740468a
--- /dev/null
+++ b/src/verso/Verso/Finished.lean
@@ -0,0 +1,84 @@
+module
+import Verso.Doc
+
+public import Lean.Data.Json.Basic
+public import Lean.Data.NameMap.Basic
+import Lean.Log
+
+set_option doc.verso true
+set_option pp.rawOnError true
+
+namespace Verso.Doc.Elab
+open Lean
+
+/--
+When elaborating document structures, we are building an internal
+representation ({lit}`IR`) relative to an unspecified {name}`Genre` that must
+be consistent for the entire elaborated structure once that structure is
+serialized and deserialized.
+-/
+opaque genre : Genre
+
+public inductive FinishedPart where
+  | mk (titleSyntax : Syntax)
+       (expandedTitle : Array Term)
+       (titlePreview : String)
+       (metadata : Option Term)
+       (blocks : Array Term)
+       (subParts : Array FinishedPart)
+       (endPos : String.Pos.Raw)
+    /-- A name representing an external module document -/
+  | included (name : Ident)
+deriving Repr, BEq
+
+/--
+Partially-serializable document structures "bottom out" at syntax nodes, which
+we don't directly serialize. Instead, when we are serializing a
+partially-serializable data structure and reach a syntax node, we store the
+syntax node in a {name}`SerializableAux` table and serialize an index into the table.
+-/
+public structure SerializableAux where
+  /-- Syntax denoting values of type {lean}`Verso.Doc.Inline genre` for some implicit {name}`genre`. -/
+  inlines : Array Term := #[]
+  /-- Syntax denoting values of type {lean}`Verso.Doc.Block genre` for some implicit {name}`genre`. -/
+  blocks : Array Term := #[]
+  /-- Syntax denoting values of type {lean}`genre.PartMetadata` for some implicit {name}`genre`. -/
+  partMetadata : Array Term := #[]
+  /-- Other modules -/
+  docs : NameSet := {}
+
+
+public partial def FinishedPart.serialize [Monad m] [MonadRef m] [MonadQuotation m] : FinishedPart → StateT SerializableAux m Lean.Json
+  | .mk _titleSyntax title titlePreview metadata blocks subParts _endPos => do
+    let aux ← get
+
+    let titleJson := title.mapIdx (fun n _ => .num <| n + aux.inlines.size)
+
+    let metadataJson ← match metadata with
+      | .none => pure Json.null
+      | .some s =>
+        let n := aux.partMetadata.size
+        set { aux with partMetadata := aux.partMetadata.push s }
+        pure <| Json.arr #[.num n]
+
+    let contentJson := blocks.mapIdx (fun n _ => .num <| n + aux.blocks.size)
+
+    set ({ aux with
+      inlines := aux.inlines ++ title
+      blocks := aux.blocks ++ blocks })
+
+    let subPartsJson ← subParts.mapM serialize
+
+    return .mkObj [
+      ("title", .arr titleJson),
+      ("titleString", .str titlePreview),
+      ("metadata", metadataJson),
+      ("content", .arr contentJson),
+      ("subParts", .arr subPartsJson),
+    ]
+
+  | .included name => do
+    modify (fun aux => { aux with docs := aux.docs.insert name.getId })
+    -- NB: deserialization depends on the implementation-defined behavior
+    -- that this will be a string
+    return ToJson.toJson name.getId
diff --git a/src/verso/Verso/VersoDoc.lean b/src/verso/Verso/VersoDoc.lean
new file mode 100644
index 00000000..ea33106e
--- /dev/null
+++ b/src/verso/Verso/VersoDoc.lean
@@ -0,0 +1,114 @@
+module
+public import Verso.Doc
+public import SubVerso.Highlighting
+
+set_option doc.verso true
+set_option pp.rawOnError true
+
+namespace Verso.Doc
+open Lean
+
+/--
+Deserializing a partially-serialized document syntax is done with access to a structure that fills
+in the parts of the document structure that weren't serialized.
+-/
+public structure DeserializeAux (genre : Genre) : Type where
+  inlines : Array (Inline genre)
+  blocks : Array (Block genre)
+  partMetadata : Array genre.PartMetadata
+  /-- Sorted by {name}`Name.quickLt` -/
+  docs : Array (Name × Part genre)
+deriving Inhabited
+
+public structure DocReconstruction where
+  highlightDeduplication : SubVerso.Highlighting.Export
+
+/--
+The result type of values created by Verso's {lit}`#doc` and {lit}`#docs` commands. A value of type
+{lean}`VersoDoc` represents a not-fully-evaluated document of type {lean}`Part` that can be turned
+into a value by invoking the `VersoDoc.toPart` method. The actual structure of a {lean}`VersoDoc`
+should not be relied on.
+-/
+public inductive VersoDoc (genre : Genre) where
+  | serialized
+      (aux : DocReconstruction → DeserializeAux genre)
+      (doc : String)
+      (docReconstructionData : String := "{}")
+      (replacementMetadata? : Option (Option genre.PartMetadata) := .none)
+  | literal (part : Part genre)
+
+instance : Inhabited (VersoDoc genre) where
+  default := VersoDoc.serialized (fun _ => Inhabited.default) "invalid" "{}" .none
+
+/--
+Replace the top-level metadata in a VersoDoc.
+-/
+public def VersoDoc.withMetadata (metadata? : Option genre.PartMetadata) : VersoDoc genre → VersoDoc genre
+  | .serialized aux doc docReconstStr _replacementMetadata? =>
+    .serialized aux doc docReconstStr (.some metadata?)
+  | .literal part =>
+    .literal { part with metadata := metadata? }
+
+def _root_.Lean.Json.getArr! (json : Json) : Array Json :=
+  match json.getArr? with
+    | .ok arr => arr
+    | .error e => panic s!"getArr! {e}"
+
+def _root_.Lean.Json.getStr! (json : Json) : String :=
+  match json.getStr? with
+    | .ok arr => arr
+    | .error e => panic s!"getStr! {e}"
+
+public partial def Part.deserialize : Json → ReaderM (DeserializeAux genre) (Part genre)
+  | name@(.str _) => do
+    let .ok id := FromJson.fromJson? name
+      | panic! "Failed to deserialize as id `{name}`"
+    let .some (_, part) := (← read).docs.binSearch (id, default) (fun (a, _) (b, _) => Name.quickLt a b)
+      | panic! "Failed to find id `{id}`"
+    return part
+  | .obj o => do
+    let aux ← read
+    let title := o.get! "title" |>.getArr! |>.map (match ·.getNat? with
+      | .ok n => match aux.inlines[n]? with
+        | .some t => t
+        | .none => panic! s!"out of bound inline: {n} vs {aux.inlines.size}"
+      | .error e => panic! s!"Ill-formed JSON part serialization (title) {e}")
+    let titleString := o.get! "titleString" |>.getStr!
+    let metadata := match o.get! "metadata" with
+      | .null => .none
+      | .arr #[.num (n : Nat)] =>
+        match (aux.partMetadata[n]?) with
+          | .some s => .some s
+          | .none => panic s!"Ill-formed JSON part serialization (metadata) {n}"
+      | json => panic! s!"Ill-formed JSON part serialization (metadata) {json}"
+    let content := o.get! "content" |>.getArr! |>.map (match ·.getNat? with
+      | .ok n => match aux.blocks[n]? with
+        | .some t => t
+        | .none => panic! s!"out of bound block: {n} vs {aux.blocks.size}"
+      | .error e => panic! s!"Ill-formed JSON part serialization (content) {e}")
+    let subParts ← o.get! "subParts" |>.getArr! |>.mapM deserialize
+    return Part.mk title titleString metadata content subParts
+  | json => panic s!"Ill-formed JSON part serialization {json}"
+
+/--
+A {lean}`VersoDoc` represents a potentially-not-fully-evaluated {lean}`Part`. Calling {lean}`VersoDoc.toPart` forces
+evaluation of the {lean}`VersoDoc` to a {lean}`Part`.
+-/
+public def VersoDoc.toPart: VersoDoc genre → Part genre
+  | .serialized auxFn docStr highlight replacementMetadata? =>
+    match (Json.parse highlight, Json.parse docStr) with
+    | (.error e, _) => panic! s!"Failed to parse VersoDoc's Export data as JSON: {e}"
+    | (_, .error e) => panic! s!"Failed to parse doc data as JSON: {e}"
+    | (.ok reconJson, .ok docJson) =>
+      if let .ok highlightJson := reconJson.getObjVal? "highlight" then
+        match SubVerso.Highlighting.Export.fromJson? highlightJson with
+        | .error e => panic! s!"Failed to deserialize Export data from parsed JSON: {e}"
+        | .ok table =>
+          let aux := auxFn ⟨table⟩
+          let part := Id.run <| ReaderT.run (Part.deserialize docJson) aux
+          match replacementMetadata? with
+          | .none => part
+          | .some replacementMetadata => { part with metadata := replacementMetadata }
+      else
+        Id.run <| ReaderT.run (Part.deserialize docJson) (auxFn ⟨{}⟩)
+  | .literal part => part

From 39b88371c2f25d7a03198856a18052520d3d2599 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sat, 27 Dec 2025 19:43:37 -0500
Subject: [PATCH 2/5] Fix metadata serialization

---
 src/tests/Tests/Elab.lean     |  1 +
 src/verso/Verso/Finished.lean | 12 +++++-------
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/tests/Tests/Elab.lean b/src/tests/Tests/Elab.lean
index dc6f8576..e832e546 100644
--- a/src/tests/Tests/Elab.lean
+++ b/src/tests/Tests/Elab.lean
@@ -75,3 +75,4 @@ A variable like {lean}`(_ : Nat)`.
 :::::::
 A variable like {lean}`_`.
 :::::::
+
diff --git a/src/verso/Verso/Finished.lean b/src/verso/Verso/Finished.lean
index c740468a..b5ee13f4 100644
--- a/src/verso/Verso/Finished.lean
+++ b/src/verso/Verso/Finished.lean
@@ -51,9 +51,13 @@ public structure SerializableAux where
 public partial def FinishedPart.serialize [Monad m] [MonadRef m] [MonadQuotation m] : FinishedPart → StateT SerializableAux m Lean.Json
   | .mk _titleSyntax title titlePreview metadata blocks subParts _endPos => do
     let aux ← get
-
     let titleJson := title.mapIdx (fun n _ => .num <| n + aux.inlines.size)
+    let contentJson := blocks.mapIdx (fun n _ => .num <| n + aux.blocks.size)
+    set ({ aux with
+      inlines := aux.inlines ++ title
+      blocks := aux.blocks ++ blocks })
 
+    let aux ← get
     let metadataJson ← match metadata with
       | .none => pure Json.null
       | .some s =>
@@ -61,12 +65,6 @@ public partial def FinishedPart.serialize [Monad m] [MonadRef m] [MonadQuotation
         set { aux with partMetadata := aux.partMetadata.push s }
         pure <| Json.arr #[.num n]
 
-    let contentJson := blocks.mapIdx (fun n _ => .num <| n + aux.blocks.size)
-
-    set ({ aux with
-      inlines := aux.inlines ++ title
-      blocks := aux.blocks ++ blocks })
-
     let subPartsJson ← subParts.mapM serialize
 
     return .mkObj [

From 9b6f5256c44dfd0a3880ca9ea5116b543d925a3f Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sat, 27 Dec 2025 20:20:05 -0500
Subject: [PATCH 3/5] Docstrings and refactor VersoDoc to DocThunk

---
 src/tests/TestMain.lean                       |   4 +-
 src/tests/Tests/Basic.lean                    |  16 +--
 src/tests/Tests/GenericCode.lean              |   6 +-
 src/tests/Tests/LeanCode.lean                 |   2 +-
 src/tests/Tests/Refs.lean                     |  16 +--
 .../VersoBlog/LiterateLeanPage.lean           |   2 +-
 .../VersoBlog/LiterateModuleDocs.lean         |   2 +-
 .../VersoLiterate/Exported.lean               |   4 +-
 src/verso-literate/VersoLiterate/Module.lean  |   2 +-
 src/verso-manual/VersoManual/Literate.lean    |   2 +-
 src/verso/Verso/Doc/Concrete.lean             |   4 +-
 src/verso/Verso/Doc/Elab/Basic.lean           |   2 +-
 src/verso/Verso/Doc/Elab/Monad.lean           |   6 +-
 src/verso/Verso/Finished.lean                 |  50 ++++++---
 src/verso/Verso/VersoDoc.lean                 | 102 ++++++++++--------
 15 files changed, 124 insertions(+), 96 deletions(-)

diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean
index f99eba17..81122106 100644
--- a/src/tests/TestMain.lean
+++ b/src/tests/TestMain.lean
@@ -36,7 +36,7 @@ Tests manual-genre TeX generation. `dir` is a subdirectory specific to a particu
 which is where actual output should go, and which contains the expected output directory.
 `doc` is the document to be rendered.
 -/
-def testTexOutput (dir : System.FilePath) (doc : Verso.Doc.VersoDoc Verso.Genre.Manual) :
+def testTexOutput (dir : System.FilePath) (doc : Verso.Doc.DocThunk Verso.Genre.Manual) :
     Config →  IO Unit := fun config =>
   let versoConfig : Verso.Genre.Manual.Config := {
     destination := "src/tests/integration" / dir / "output",
@@ -47,7 +47,7 @@ def testTexOutput (dir : System.FilePath) (doc : Verso.Doc.VersoDoc Verso.Genre.
   let runTest : IO Unit  :=
     open Verso Genre Manual in do
     let logError (msg : String) := IO.eprintln msg
-    ReaderT.run (emitTeX logError versoConfig doc.toPart) extension_impls%
+    ReaderT.run (emitTeX logError versoConfig doc.force) extension_impls%
 
   Verso.Integration.runTests {
     testDir := "src/tests/integration" / dir,
diff --git a/src/tests/Tests/Basic.lean b/src/tests/Tests/Basic.lean
index 7d60c110..85071410 100644
--- a/src/tests/Tests/Basic.lean
+++ b/src/tests/Tests/Basic.lean
@@ -16,7 +16,7 @@ set_option pp.rawOnError true
 :::::::
 /-- info: Verso.Doc.Part.mk #[Verso.Doc.Inline.text "Nothing"] "Nothing" none #[] #[] -/
 #guard_msgs in
-  #eval noDoc.toPart
+  #eval noDoc.force
 
 
 /- ----- -/
@@ -36,7 +36,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval littleParagraph.toPart
+  #eval littleParagraph.force
 
 
 /- ----- -/
@@ -56,7 +56,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval listOneItem.toPart
+  #eval listOneItem.force
 
 
 /- ----- -/
@@ -83,7 +83,7 @@ info: Verso.Doc.Part.mk
       #[]]
 -/
 #guard_msgs in
-  #eval sectionAndPara.toPart
+  #eval sectionAndPara.force
 
 
 /- ----- -/
@@ -128,7 +128,7 @@ info: Verso.Doc.Part.mk
           #[]]]
 -/
 #guard_msgs in
-  #eval nestedDoc1.toPart
+  #eval nestedDoc1.force
 
 
 /- ----- -/
@@ -173,7 +173,7 @@ info: Verso.Doc.Part.mk
           #[]]]
 -/
 #guard_msgs in
-  #eval nestedDoc2.toPart
+  #eval nestedDoc2.force
 
 
 /- ----- -/
@@ -223,7 +223,7 @@ info: Verso.Doc.Part.mk
           #[]]]
 -/
 #guard_msgs in
-  #eval nestedDoc3.toPart
+  #eval nestedDoc3.force
 
 
 /- ----- -/
@@ -260,7 +260,7 @@ info: Verso.Doc.Part.mk
       #[]]
 -/
 #guard_msgs in
-  #eval nestedDoc4.toPart
+  #eval nestedDoc4.force
 
 
 /- ----- -/
diff --git a/src/tests/Tests/GenericCode.lean b/src/tests/Tests/GenericCode.lean
index 9ad227cf..38dd19ea 100644
--- a/src/tests/Tests/GenericCode.lean
+++ b/src/tests/Tests/GenericCode.lean
@@ -39,7 +39,7 @@ info: Verso.Doc.Part.mk
       #[]]
 -/
 #guard_msgs in
-  #eval code1.toPart
+  #eval code1.force
 /--
 info: Verso.Output.Html.tag
   "section"
@@ -58,7 +58,7 @@ info: Verso.Output.Html.tag
               (Verso.Output.Html.text true "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n")])])
 -/
 #guard_msgs in
-  #eval Doc.Genre.none.toHtml (m:=Id) {logError := fun _ => ()} () () {} {} {} code1.toPart |>.run .empty |>.fst
+  #eval Doc.Genre.none.toHtml (m:=Id) {logError := fun _ => ()} () () {} {} {} code1.force |>.run .empty |>.fst
 
 
 /- ----- -/
@@ -92,4 +92,4 @@ info: Verso.Doc.Part.mk
       #[]]
 -/
 #guard_msgs in
-  #eval code2.toPart
+  #eval code2.force
diff --git a/src/tests/Tests/LeanCode.lean b/src/tests/Tests/LeanCode.lean
index a20e59da..d10124ad 100644
--- a/src/tests/Tests/LeanCode.lean
+++ b/src/tests/Tests/LeanCode.lean
@@ -70,7 +70,7 @@ info: (some (Verso.Genre.Manual.InlineLean.Inline.lean, [{"seq":
      {"tok": {"kind": {"withType": {"type": "Nat"}}, "content": "3"}}}]}},
  []]))-/
 #guard_msgs in
-#eval match inspect.toPart.content[0]! with
+#eval match inspect.force.content[0]! with
   | .para x => match x[0]! with
     | .other code _ => Option.some (code.name, code.data)
     | _ => .none
diff --git a/src/tests/Tests/Refs.lean b/src/tests/Tests/Refs.lean
index 6da95723..b36250bf 100644
--- a/src/tests/Tests/Refs.lean
+++ b/src/tests/Tests/Refs.lean
@@ -24,7 +24,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval regularLink.toPart
+  #eval regularLink.force
 
 
 /- ----- -/
@@ -46,7 +46,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval refLink.toPart
+  #eval refLink.force
 
 
 /- ----- -/
@@ -68,7 +68,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval noteLink.toPart
+  #eval noteLink.force
 
 
 /- ----- -/
@@ -95,7 +95,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval refAndLink.toPart
+  #eval refAndLink.force
 
 #docs (.none) refAndLink2 "Ref/link ordering" :=
 :::::::
@@ -123,13 +123,13 @@ Here's [a link][to here][^note]!
 :::::::
 
 /-- info: true -/
-#guard_msgs in #eval refAndLink.toPart == refAndLink2.toPart
+#guard_msgs in #eval refAndLink.force == refAndLink2.force
 
 /-- info: true -/
-#guard_msgs in #eval refAndLink.toPart == refAndLink3.toPart
+#guard_msgs in #eval refAndLink.force == refAndLink3.force
 
 /-- info: true -/
-#guard_msgs in #eval refAndLink.toPart == refAndLink4.toPart
+#guard_msgs in #eval refAndLink.force == refAndLink4.force
 
 #docs (.none) refAndLinkRecursion "Ref/link recursion" :=
 :::::::
@@ -162,7 +162,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval refAndLinkRecursion.toPart
+  #eval refAndLinkRecursion.force
 
 /--
 error: Already defined link [foo] as 'https://example.com'
diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean
index 7023fa6a..5f541da2 100644
--- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean
+++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean
@@ -528,7 +528,7 @@ def elabLiteratePage (x : Ident) (path : StrLit) (mod : Ident) (config : LitPage
       | _ => p
     else finished
 
-  let ty ← ``(VersoDoc $genre)
+  let ty ← ``(DocThunk $genre)
   let doc ← Command.runTermElabM fun _ => finished.toVersoDoc genre ctx docState partState
   elabCommand <| ← `(def $x : $ty := $doc)
 
diff --git a/src/verso-blog/VersoBlog/LiterateModuleDocs.lean b/src/verso-blog/VersoBlog/LiterateModuleDocs.lean
index 90973e73..fe351779 100644
--- a/src/verso-blog/VersoBlog/LiterateModuleDocs.lean
+++ b/src/verso-blog/VersoBlog/LiterateModuleDocs.lean
@@ -78,7 +78,7 @@ def elabFromModuleDocs (x : Ident) (path : StrLit) (mod : Ident) (title : StrLit
     let title ← Meta.mkArrayLit (.app (mkConst ``Verso.Doc.Inline) g) title.toList
     withOptions (Compiler.LCNF.compiler.extract_closed.set · false) do
       addAndCompile <| .defnDecl {
-        name, levelParams := [], type := .app (mkConst ``Verso.Doc.VersoDoc) g,
+        name, levelParams := [], type := .app (mkConst ``Verso.Doc.DocThunk) g,
         value := ← Meta.mkAppM ``modToPage! #[
           ← Meta.mkAppM ``VersoLiterate.loadJsonString! #[mkConst jsonName, mkStrLit s!"JSON for {x.getId}"],
           title,
diff --git a/src/verso-literate/VersoLiterate/Exported.lean b/src/verso-literate/VersoLiterate/Exported.lean
index 35bab2ff..5e5a090e 100644
--- a/src/verso-literate/VersoLiterate/Exported.lean
+++ b/src/verso-literate/VersoLiterate/Exported.lean
@@ -247,7 +247,7 @@ private partial def mdBlock : MD4Lean.Block → Except String (Block g)
   | .html .. => throw "Literal HTML in Markdown not supported"
   | .hr => throw "Thematic break (horizontal rule) in Markdown not supported"
 
-partial def modToPage [LoadLiterate g] (mod : LitMod) (title : Array (Inline g)) (titleString : String) : Except String (VersoDoc g) := do
+partial def modToPage [LoadLiterate g] (mod : LitMod) (title : Array (Inline g)) (titleString : String) : Except String (DocThunk g) := do
   let mut stack : Array (Part g) := #[]
   let mut p : Part g := {title, titleString, metadata := none, content := #[], subParts := #[]}
 
@@ -305,7 +305,7 @@ partial def modToPage [LoadLiterate g] (mod : LitMod) (title : Array (Inline g))
     let p' := stack.back
     stack := stack.pop
     p := pushPart p' p
-  return VersoDoc.literal p
+  return DocThunk.value p
 where
   docstringBlock (doc : LitVersoDocString) : Array (Block g) :=
     let parts := doc.subsections.map loadPart
diff --git a/src/verso-literate/VersoLiterate/Module.lean b/src/verso-literate/VersoLiterate/Module.lean
index 93c6c22a..01587015 100644
--- a/src/verso-literate/VersoLiterate/Module.lean
+++ b/src/verso-literate/VersoLiterate/Module.lean
@@ -30,7 +30,7 @@ def load (jsonFile : System.FilePath) : IO LitMod := do
   | .error e => throw <| .userError e
   | .ok v => pure v
 
-def modToPage! [LoadLiterate g] (mod : LitMod) (title : Array (Inline g)) (titleString : String) : VersoDoc g :=
+def modToPage! [LoadLiterate g] (mod : LitMod) (title : Array (Inline g)) (titleString : String) : DocThunk g :=
   match modToPage mod title titleString with
   | .error e => panic! s!"Couldn't load {titleString}: {e}"
   | .ok v => v
diff --git a/src/verso-manual/VersoManual/Literate.lean b/src/verso-manual/VersoManual/Literate.lean
index 1ba194a2..06b68fed 100644
--- a/src/verso-manual/VersoManual/Literate.lean
+++ b/src/verso-manual/VersoManual/Literate.lean
@@ -101,7 +101,7 @@ def getModuleWithDocs (path : StrLit) (mod : Ident) (title : StrLit) : PartElabM
     let title ← Meta.mkArrayLit (.app (mkConst ``Verso.Doc.Inline) g) title.toList
     withOptions (Compiler.LCNF.compiler.extract_closed.set · false) do
       addAndCompile <| .defnDecl {
-        name, levelParams := [], type := .app (mkConst ``Verso.Doc.VersoDoc) g,
+        name, levelParams := [], type := .app (mkConst ``Verso.Doc.DocThunk) g,
         value := ← Meta.mkAppM ``modToPage! #[
           ← Meta.mkAppM ``VersoLiterate.loadJsonString! #[mkConst jsonName, mkStrLit s!"JSON for {mod.getId}"],
           title,
diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
index a8594e95..f0b9d764 100644
--- a/src/verso/Verso/Doc/Concrete.lean
+++ b/src/verso/Verso/Doc/Concrete.lean
@@ -97,7 +97,7 @@ elab "#docs" "(" genre:term ")" n:ident title:str ":=" ":::::::" text:document "
       | none => panic! "No final token!"
     | _ => panic! "Nothing"
   let doc ← Command.runTermElabM fun _ => elabDoc genre title text.raw.getArgs endTok.getPos!
-  Command.elabCommand (← `(def $n : VersoDoc $genre := $doc))
+  Command.elabCommand (← `(def $n : DocThunk $genre := $doc))
 
 elab "#doc" "(" genre:term ")" title:str "=>" text:completeDocument eoi : term => do
   findGenreTm genre
@@ -216,7 +216,7 @@ private meta def finishDoc (genreSyntax : Term) (title : StrLit) : Command.Comma
 
   let n := mkIdentFrom title (← currentDocName)
   let doc ← Command.runTermElabM fun _ => finished.toVersoDoc genreSyntax versoEnv.ctx versoEnv.docState versoEnv.partState
-  let ty ← ``(VersoDoc $genreSyntax)
+  let ty ← ``(DocThunk $genreSyntax)
   Command.elabCommand (← `(def $n : $ty := $doc))
 
 syntax (name := replaceDoc) "#doc" "(" term ")" str "=>" : command
diff --git a/src/verso/Verso/Doc/Elab/Basic.lean b/src/verso/Verso/Doc/Elab/Basic.lean
index f4b88771..b319410d 100644
--- a/src/verso/Verso/Doc/Elab/Basic.lean
+++ b/src/verso/Verso/Doc/Elab/Basic.lean
@@ -37,7 +37,7 @@ public partial def FinishedPart.toSyntax [Monad m] [MonadQuotation m]
     -- let bindings introduced by "chunking" the elaboration may fail to infer types
     let typedBlocks ← blocks.mapM fun b => `(($b : Block $genre))
     ``(Part.mk #[$titleInlines,*] $(quote titleString) $metaStx #[$typedBlocks,*] #[$subStx,*])
-  | .included name => ``(VersoDoc.toPart $name)
+  | .included name => ``(DocThunk.force $name)
 
 public partial def FinishedPart.toTOC : FinishedPart → TOC
   | .mk titleStx _titleInlines titleString _metadata _blocks subParts endPos =>
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index 5e99fea7..618b0d9f 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -468,12 +468,12 @@ public def quoteSerializableAux [Monad m] [MonadQuotation m]
     (aux : Doc.Elab.SerializableAux)
     : m Term := do
   let sortedDocs := aux.docs.toArray.qsort (lt := Name.quickLt)
-  let quotedDocs ← sortedDocs.mapM (fun name => ``(Prod.mk $(quote name) (VersoDoc.toPart $(mkIdent name))))
+  let quotedDocs ← sortedDocs.mapM (fun name => ``(Prod.mk $(quote name) (DocThunk.force $(mkIdent name))))
   ``(Doc.DeserializeAux.mk #[$aux.inlines,*] #[$aux.blocks,*] #[$aux.partMetadata,*] #[$quotedDocs,*])
 
 
 /--
-Creates a term denoting a {lean}`VersoDoc` value from a {lean}`FinishedPart`. This is the final step
+Creates a term denoting a {lean}`DocThunk` value from a {lean}`FinishedPart`. This is the final step
 in turning a parsed verso doc into syntax.
 -/
 public def FinishedPart.toVersoDoc
@@ -544,7 +544,7 @@ public def FinishedPart.toVersoDoc
     | .none => Json.mkObj []
     | .some table => Json.mkObj [("highlight", table.toExport.toJson)]
 
-  ``(VersoDoc.serialized (fun $docReconstructionPlaceholder => $quotedAux) $(quote partJson.compress) $(quote reconstJson.compress) none)
+  ``(DocThunk.serialized (fun $docReconstructionPlaceholder => $quotedAux) $(quote partJson.compress) $(quote reconstJson.compress) none)
 
 
 public abbrev BlockExpander := Syntax → DocElabM (TSyntax `term)
diff --git a/src/verso/Verso/Finished.lean b/src/verso/Verso/Finished.lean
index b5ee13f4..ea51de34 100644
--- a/src/verso/Verso/Finished.lean
+++ b/src/verso/Verso/Finished.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Rob Simmons
+-/
 module
 import Verso.Doc
 
@@ -19,6 +24,30 @@ serialized and deserialized.
 -/
 opaque genre : Genre
 
+/--
+Partially-serializable document structures can potentially "bottom out" as non-serializable data,
+represented as a {name}`Term` that, if elaborated and evaluated, represents part of a document.
+
+When serializing a partially-serializable document, these non-serializable segments are stored in
+a {name}`SerializableAux` data structure, and the serializable data contains an index into this
+data structure.
+
+To de-serialize the document, the terms in the data structure must be elaborated and evaluated to
+document data of the appropriate genre.
+-/
+public structure SerializableAux where
+  /-- Syntax denoting values of type {lean}`Verso.Doc.Inline genre` for some implicit {name}`genre`. -/
+  inlines : Array Term := #[]
+  /-- Syntax denoting values of type {lean}`Verso.Doc.Block genre` for some implicit {name}`genre`. -/
+  blocks : Array Term := #[]
+  /-- Syntax denoting values of type {lean}`genre.PartMetadata` for some implicit {name}`genre`. -/
+  partMetadata : Array Term := #[]
+  /-- Other modules referenced in this document by name -/
+  docs : NameSet := {}
+
+/--
+A {name}`FinishedPart` is the result of elaborating a document's part structure.
+-/
 public inductive FinishedPart where
   | mk (titleSyntax : Syntax)
        (expandedTitle : Array Term)
@@ -27,28 +56,15 @@ public inductive FinishedPart where
        (blocks : Array Term)
        (subParts : Array FinishedPart)
        (endPos : String.Pos.Raw)
-    /-- A name representing an external module document -/
+    /-- A name representing a Part-structured document in another module -/
   | included (name : Ident)
 deriving Repr, BEq
 
 /--
-Partially-serializable document structures "bottom out" at syntax nodes, which
-we don't directly serialize. Instead, when we are serializing a
-partially-serializable data structure and reach a syntax node, we store the
-syntax node in a {name}`SerializableAux` table and serialize an index into the table.
+Transform a {name}`FinishedPart` into {name}`Json`, extracting any non-serializable data in the
+{name}`SerializableAux` data structure.
 -/
-public structure SerializableAux where
-  /-- Syntax denoting values of type {lean}`Verso.Doc.Inline genre` for some implicit {name}`genre`. -/
-  inlines : Array Term := #[]
-  /-- Syntax denoting values of type {lean}`Verso.Doc.Block genre` for some implicit {name}`genre`. -/
-  blocks : Array Term := #[]
-  /-- Syntax denoting values of type {lean}`genre.PartMetadata` for some implicit {name}`genre`. -/
-  partMetadata : Array Term := #[]
-  /-- Other modules -/
-  docs : NameSet := {}
-
-
-public partial def FinishedPart.serialize [Monad m] [MonadRef m] [MonadQuotation m] : FinishedPart → StateT SerializableAux m Lean.Json
+public partial def FinishedPart.serialize [Monad m] [MonadRef m] [MonadQuotation m] : FinishedPart → StateT SerializableAux m Json
   | .mk _titleSyntax title titlePreview metadata blocks subParts _endPos => do
     let aux ← get
     let titleJson := title.mapIdx (fun n _ => .num <| n + aux.inlines.size)
diff --git a/src/verso/Verso/VersoDoc.lean b/src/verso/Verso/VersoDoc.lean
index ea33106e..26235055 100644
--- a/src/verso/Verso/VersoDoc.lean
+++ b/src/verso/Verso/VersoDoc.lean
@@ -1,6 +1,12 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Rob Simmons
+-/
 module
 public import Verso.Doc
 public import SubVerso.Highlighting
+import Verso.Finished
 
 set_option doc.verso true
 set_option pp.rawOnError true
@@ -20,45 +26,11 @@ public structure DeserializeAux (genre : Genre) : Type where
   docs : Array (Name × Part genre)
 deriving Inhabited
 
-public structure DocReconstruction where
-  highlightDeduplication : SubVerso.Highlighting.Export
 
 /--
-The result type of values created by Verso's {lit}`#doc` and {lit}`#docs` commands. A value of type
-{lean}`VersoDoc` represents a not-fully-evaluated document of type {lean}`Part` that can be turned
-into a value by invoking the `VersoDoc.toPart` method. The actual structure of a {lean}`VersoDoc`
-should not be relied on.
+Transform a previously-serialized {name (full := Elab.FinishedPart)}`FinishedPart` into a
+{name}`Part`.
 -/
-public inductive VersoDoc (genre : Genre) where
-  | serialized
-      (aux : DocReconstruction → DeserializeAux genre)
-      (doc : String)
-      (docReconstructionData : String := "{}")
-      (replacementMetadata? : Option (Option genre.PartMetadata) := .none)
-  | literal (part : Part genre)
-
-instance : Inhabited (VersoDoc genre) where
-  default := VersoDoc.serialized (fun _ => Inhabited.default) "invalid" "{}" .none
-
-/--
-Replace the top-level metadata in a VersoDoc.
--/
-public def VersoDoc.withMetadata (metadata? : Option genre.PartMetadata) : VersoDoc genre → VersoDoc genre
-  | .serialized aux doc docReconstStr _replacementMetadata? =>
-    .serialized aux doc docReconstStr (.some metadata?)
-  | .literal part =>
-    .literal { part with metadata := metadata? }
-
-def _root_.Lean.Json.getArr! (json : Json) : Array Json :=
-  match json.getArr? with
-    | .ok arr => arr
-    | .error e => panic s!"getArr! {e}"
-
-def _root_.Lean.Json.getStr! (json : Json) : String :=
-  match json.getStr? with
-    | .ok arr => arr
-    | .error e => panic s!"getStr! {e}"
-
 public partial def Part.deserialize : Json → ReaderM (DeserializeAux genre) (Part genre)
   | name@(.str _) => do
     let .ok id := FromJson.fromJson? name
@@ -68,33 +40,73 @@ public partial def Part.deserialize : Json → ReaderM (DeserializeAux genre) (P
     return part
   | .obj o => do
     let aux ← read
-    let title := o.get! "title" |>.getArr! |>.map (match ·.getNat? with
+    let titleArr := match o.get! "title" |>.getArr? with
+      | .ok arr => arr
+      | .error e => panic! s!"ill-formed JSON part serialization (title) {e}"
+    let title := titleArr.map (match ·.getNat? with
       | .ok n => match aux.inlines[n]? with
         | .some t => t
         | .none => panic! s!"out of bound inline: {n} vs {aux.inlines.size}"
       | .error e => panic! s!"Ill-formed JSON part serialization (title) {e}")
-    let titleString := o.get! "titleString" |>.getStr!
+    let titleString := match o.get! "titleString" |>.getStr? with
+      | .ok str => str
+      | .error e => panic! panic! s!"Ill-formed JSON part serialization (titleString) {e}"
     let metadata := match o.get! "metadata" with
       | .null => .none
       | .arr #[.num (n : Nat)] =>
         match (aux.partMetadata[n]?) with
           | .some s => .some s
-          | .none => panic s!"Ill-formed JSON part serialization (metadata) {n}"
+          | .none => panic! s!"Ill-formed JSON part serialization (metadata) {n}"
       | json => panic! s!"Ill-formed JSON part serialization (metadata) {json}"
-    let content := o.get! "content" |>.getArr! |>.map (match ·.getNat? with
+    let contentArr := match o.get! "content" |>.getArr? with
+      | .ok arr => arr
+      | .error e => panic! s!"Ill-formed JSON part serialization (content) {e}"
+    let content := contentArr.map (match ·.getNat? with
       | .ok n => match aux.blocks[n]? with
         | .some t => t
         | .none => panic! s!"out of bound block: {n} vs {aux.blocks.size}"
       | .error e => panic! s!"Ill-formed JSON part serialization (content) {e}")
-    let subParts ← o.get! "subParts" |>.getArr! |>.mapM deserialize
+    let subPartsArr := match o.get! "subParts" |>.getArr? with
+      | .ok arr => arr
+      | .error e => panic! s!"Ill-formed JSON part serialization (subParts) {e}"
+    let subParts ← subPartsArr.mapM deserialize
     return Part.mk title titleString metadata content subParts
   | json => panic s!"Ill-formed JSON part serialization {json}"
 
+public structure DocReconstruction where
+  highlightDeduplication : SubVerso.Highlighting.Export
+
+/--
+The result type of values created by Verso's {lit}`#doc` and {lit}`#docs` commands. A value of type
+{lean}`DocThunk` represents a partially-serialized value of type {lean}`Part` that can be turned
+into a value by invoking the `DocThunk.force` method. The actual structure of a {lean}`DocThunk`
+should not be relied on.
+-/
+public inductive DocThunk (genre : Genre) where
+  | serialized
+      (aux : DocReconstruction → DeserializeAux genre)
+      (doc : String)
+      (docReconstructionData : String := "{}")
+      (replacementMetadata? : Option (Option genre.PartMetadata) := .none)
+  | value (part : Part genre)
+
+instance : Inhabited (DocThunk genre) where
+  default := DocThunk.value default
+
+/--
+Replace the top-level metadata in a {name}`DocThunk` without forcing the thunk.
+-/
+public def DocThunk.withMetadata (metadata? : Option genre.PartMetadata) : DocThunk genre → DocThunk genre
+  | .serialized aux doc docReconstStr _replacementMetadata? =>
+    .serialized aux doc docReconstStr (.some metadata?)
+  | .value part =>
+    .value { part with metadata := metadata? }
+
 /--
-A {lean}`VersoDoc` represents a potentially-not-fully-evaluated {lean}`Part`. Calling {lean}`VersoDoc.toPart` forces
-evaluation of the {lean}`VersoDoc` to a {lean}`Part`.
+A {lean}`DocThunk` represents a potentially-not-fully-evaluated {lean}`Part`. Calling
+{lean}`DocThunk.force` forces evaluation of the {lean}`DocThunk` to a {lean}`Part`.
 -/
-public def VersoDoc.toPart: VersoDoc genre → Part genre
+public def DocThunk.force: DocThunk genre → Part genre
   | .serialized auxFn docStr highlight replacementMetadata? =>
     match (Json.parse highlight, Json.parse docStr) with
     | (.error e, _) => panic! s!"Failed to parse VersoDoc's Export data as JSON: {e}"
@@ -111,4 +123,4 @@ public def VersoDoc.toPart: VersoDoc genre → Part genre
           | .some replacementMetadata => { part with metadata := replacementMetadata }
       else
         Id.run <| ReaderT.run (Part.deserialize docJson) (auxFn ⟨{}⟩)
-  | .literal part => part
+  | .value part => part

From 546563836f4a1cd6a41bef7206e1c5aaae3a4a49 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sat, 27 Dec 2025 23:19:42 -0500
Subject: [PATCH 4/5] Renaming

---
 src/tests/Tests/Basic.lean                    |  1 +
 src/tests/Tests/Elab.lean                     |  1 -
 src/verso/Verso.lean                          |  1 +
 .../Verso/{VersoDoc.lean => Deserialize.lean} |  4 +-
 src/verso/Verso/Doc/Concrete.lean             |  1 +
 src/verso/Verso/Doc/Elab/Basic.lean           |  4 +-
 src/verso/Verso/Doc/Elab/Monad.lean           |  4 +-
 src/verso/Verso/Doc/Name.lean                 |  6 +-
 src/verso/Verso/Finished.lean                 | 98 -------------------
 9 files changed, 12 insertions(+), 108 deletions(-)
 rename src/verso/Verso/{VersoDoc.lean => Deserialize.lean} (98%)
 delete mode 100644 src/verso/Verso/Finished.lean

diff --git a/src/tests/Tests/Basic.lean b/src/tests/Tests/Basic.lean
index 85071410..60ee0607 100644
--- a/src/tests/Tests/Basic.lean
+++ b/src/tests/Tests/Basic.lean
@@ -276,3 +276,4 @@ info: Verso.Doc.Part.mk
 #### Sub^3section
 
 :::::::
+
diff --git a/src/tests/Tests/Elab.lean b/src/tests/Tests/Elab.lean
index e832e546..dc6f8576 100644
--- a/src/tests/Tests/Elab.lean
+++ b/src/tests/Tests/Elab.lean
@@ -75,4 +75,3 @@ A variable like {lean}`(_ : Nat)`.
 :::::::
 A variable like {lean}`_`.
 :::::::
-
diff --git a/src/verso/Verso.lean b/src/verso/Verso.lean
index 47d9f8f6..7bd53cde 100644
--- a/src/verso/Verso.lean
+++ b/src/verso/Verso.lean
@@ -7,6 +7,7 @@ module
 -- This module serves as the root of the `Verso` library.
 -- Import modules here that should be built as part of the library.
 public import Verso.Code
+public import Verso.Deserialize
 public import Verso.Doc
 public import Verso.Doc.ArgParse
 public import Verso.Doc.Concrete
diff --git a/src/verso/Verso/VersoDoc.lean b/src/verso/Verso/Deserialize.lean
similarity index 98%
rename from src/verso/Verso/VersoDoc.lean
rename to src/verso/Verso/Deserialize.lean
index 26235055..02be6cd3 100644
--- a/src/verso/Verso/VersoDoc.lean
+++ b/src/verso/Verso/Deserialize.lean
@@ -6,7 +6,7 @@ Author: Rob Simmons
 module
 public import Verso.Doc
 public import SubVerso.Highlighting
-import Verso.Finished
+import Verso.Serialize
 
 set_option doc.verso true
 set_option pp.rawOnError true
@@ -109,7 +109,7 @@ A {lean}`DocThunk` represents a potentially-not-fully-evaluated {lean}`Part`. Ca
 public def DocThunk.force: DocThunk genre → Part genre
   | .serialized auxFn docStr highlight replacementMetadata? =>
     match (Json.parse highlight, Json.parse docStr) with
-    | (.error e, _) => panic! s!"Failed to parse VersoDoc's Export data as JSON: {e}"
+    | (.error e, _) => panic! s!"Failed to parse DocThunk's Export data as JSON: {e}"
     | (_, .error e) => panic! s!"Failed to parse doc data as JSON: {e}"
     | (.ok reconJson, .ok docJson) =>
       if let .ok highlightJson := reconJson.getObjVal? "highlight" then
diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
index f0b9d764..d4a9b85f 100644
--- a/src/verso/Verso/Doc/Concrete.lean
+++ b/src/verso/Verso/Doc/Concrete.lean
@@ -8,6 +8,7 @@ public import Lean.Parser.Types
 public meta import Verso.Parser
 public import Lean.Elab.Command
 public meta import SubVerso.Highlighting.Export
+import Verso.Deserialize
 import Verso.Doc
 public import Verso.Doc.Elab
 public meta import Verso.Doc.Elab.Monad
diff --git a/src/verso/Verso/Doc/Elab/Basic.lean b/src/verso/Verso/Doc/Elab/Basic.lean
index b319410d..c765c34a 100644
--- a/src/verso/Verso/Doc/Elab/Basic.lean
+++ b/src/verso/Verso/Doc/Elab/Basic.lean
@@ -5,8 +5,8 @@ Author: David Thrane Christiansen, Rob Simmons
 -/
 module
 public import Verso.Doc
-import Verso.VersoDoc
-public import Verso.Finished
+import Verso.Deserialize
+public import Verso.Serialize
 
 open Lean
 
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index 618b0d9f..f963f142 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -12,7 +12,8 @@ import Lean.Meta.Reduce
 import Lean.DocString.Syntax
 import Lean.DocString
 
-import SubVerso.Highlighting
+public import SubVerso.Highlighting
+import Verso.Deserialize
 import Verso.Doc
 public import Verso.Doc.ArgParse
 public import Verso.Doc.Elab.InlineString
@@ -21,7 +22,6 @@ public import Verso.Doc.Elab.Basic
 import Verso.Doc.Elab.ExpanderAttribute
 public import Verso.Doc.Name
 import Verso.Doc.DocName
-public import Verso.VersoDoc
 public import Verso.Instances
 
 set_option doc.verso true
diff --git a/src/verso/Verso/Doc/Name.lean b/src/verso/Verso/Doc/Name.lean
index cfec0baa..e334785f 100644
--- a/src/verso/Verso/Doc/Name.lean
+++ b/src/verso/Verso/Doc/Name.lean
@@ -28,7 +28,7 @@ theorem unDocName_docName_eq_id : unDocName ∘ docName = id := by
 /-- Treats an identifier as a module that contains Verso using the standard convention -/
 macro "%doc" moduleName:ident : term => do
   let ident := mkIdentFrom moduleName <| docName moduleName.getId
-  `($(ident).toPart)
+  `($(ident).force)
 
 /--
 Treats an identifier as a module that contains Verso using the standard convention if it exists, or
@@ -38,8 +38,8 @@ macro "%doc?" nameOrModuleName:ident : term => do
   let n := mkIdentFrom nameOrModuleName (docName nameOrModuleName.getId)
   let r ← Macro.resolveGlobalName n.getId
   let r := r.filter (·.2.isEmpty) -- ignore field access possibilities here
-  if r.isEmpty then `($(nameOrModuleName).toPart)
-  else `($(n).toPart)
+  if r.isEmpty then `($(nameOrModuleName).force)
+  else `($(n).force)
 
 macro "%docName" moduleName:ident : term =>
   let n := mkIdentFrom moduleName (docName moduleName.getId) |>.getId
diff --git a/src/verso/Verso/Finished.lean b/src/verso/Verso/Finished.lean
deleted file mode 100644
index ea51de34..00000000
--- a/src/verso/Verso/Finished.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-/-
-Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Rob Simmons
--/
-module
-import Verso.Doc
-
-public import Lean.Data.Json.Basic
-public import Lean.Data.NameMap.Basic
-import Lean.Log
-
-set_option doc.verso true
-set_option pp.rawOnError true
-
-namespace Verso.Doc.Elab
-open Lean
-
-/--
-When elaborating document structures, we are building an internal
-representation ({lit}`IR`) relative to an unspecified {name}`Genre` that must
-be consistent for the entire elaborated structure once that structure is
-serialized and deserialized.
--/
-opaque genre : Genre
-
-/--
-Partially-serializable document structures can potentially "bottom out" as non-serializable data,
-represented as a {name}`Term` that, if elaborated and evaluated, represents part of a document.
-
-When serializing a partially-serializable document, these non-serializable segments are stored in
-a {name}`SerializableAux` data structure, and the serializable data contains an index into this
-data structure.
-
-To de-serialize the document, the terms in the data structure must be elaborated and evaluated to
-document data of the appropriate genre.
--/
-public structure SerializableAux where
-  /-- Syntax denoting values of type {lean}`Verso.Doc.Inline genre` for some implicit {name}`genre`. -/
-  inlines : Array Term := #[]
-  /-- Syntax denoting values of type {lean}`Verso.Doc.Block genre` for some implicit {name}`genre`. -/
-  blocks : Array Term := #[]
-  /-- Syntax denoting values of type {lean}`genre.PartMetadata` for some implicit {name}`genre`. -/
-  partMetadata : Array Term := #[]
-  /-- Other modules referenced in this document by name -/
-  docs : NameSet := {}
-
-/--
-A {name}`FinishedPart` is the result of elaborating a document's part structure.
--/
-public inductive FinishedPart where
-  | mk (titleSyntax : Syntax)
-       (expandedTitle : Array Term)
-       (titlePreview : String)
-       (metadata : Option Term)
-       (blocks : Array Term)
-       (subParts : Array FinishedPart)
-       (endPos : String.Pos.Raw)
-    /-- A name representing a Part-structured document in another module -/
-  | included (name : Ident)
-deriving Repr, BEq
-
-/--
-Transform a {name}`FinishedPart` into {name}`Json`, extracting any non-serializable data in the
-{name}`SerializableAux` data structure.
--/
-public partial def FinishedPart.serialize [Monad m] [MonadRef m] [MonadQuotation m] : FinishedPart → StateT SerializableAux m Json
-  | .mk _titleSyntax title titlePreview metadata blocks subParts _endPos => do
-    let aux ← get
-    let titleJson := title.mapIdx (fun n _ => .num <| n + aux.inlines.size)
-    let contentJson := blocks.mapIdx (fun n _ => .num <| n + aux.blocks.size)
-    set ({ aux with
-      inlines := aux.inlines ++ title
-      blocks := aux.blocks ++ blocks })
-
-    let aux ← get
-    let metadataJson ← match metadata with
-      | .none => pure Json.null
-      | .some s =>
-        let n := aux.partMetadata.size
-        set { aux with partMetadata := aux.partMetadata.push s }
-        pure <| Json.arr #[.num n]
-
-    let subPartsJson ← subParts.mapM serialize
-
-    return .mkObj [
-      ("title", .arr titleJson),
-      ("titleString", .str titlePreview),
-      ("metadata", metadataJson),
-      ("content", .arr contentJson),
-      ("subParts", .arr subPartsJson),
-    ]
-
-  | .included name => do
-    modify (fun aux => { aux with docs := aux.docs.insert name.getId })
-    -- NB: deserialization depends on the implementation-defined behavior
-    -- that this will be a string
-    return ToJson.toJson name.getId

From bf0ba0f514fdc8c59008ade54a5e5feba864339b Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 09:56:14 -0500
Subject: [PATCH 5/5] missing file

---
 src/verso/Verso/Serialize.lean | 98 ++++++++++++++++++++++++++++++++++
 1 file changed, 98 insertions(+)
 create mode 100644 src/verso/Verso/Serialize.lean

diff --git a/src/verso/Verso/Serialize.lean b/src/verso/Verso/Serialize.lean
new file mode 100644
index 00000000..ea51de34
--- /dev/null
+++ b/src/verso/Verso/Serialize.lean
@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Rob Simmons
+-/
+module
+import Verso.Doc
+
+public import Lean.Data.Json.Basic
+public import Lean.Data.NameMap.Basic
+import Lean.Log
+
+set_option doc.verso true
+set_option pp.rawOnError true
+
+namespace Verso.Doc.Elab
+open Lean
+
+/--
+When elaborating document structures, we are building an internal
+representation ({lit}`IR`) relative to an unspecified {name}`Genre` that must
+be consistent for the entire elaborated structure once that structure is
+serialized and deserialized.
+-/
+opaque genre : Genre
+
+/--
+Partially-serializable document structures can potentially "bottom out" as non-serializable data,
+represented as a {name}`Term` that, if elaborated and evaluated, represents part of a document.
+
+When serializing a partially-serializable document, these non-serializable segments are stored in
+a {name}`SerializableAux` data structure, and the serializable data contains an index into this
+data structure.
+
+To de-serialize the document, the terms in the data structure must be elaborated and evaluated to
+document data of the appropriate genre.
+-/
+public structure SerializableAux where
+  /-- Syntax denoting values of type {lean}`Verso.Doc.Inline genre` for some implicit {name}`genre`. -/
+  inlines : Array Term := #[]
+  /-- Syntax denoting values of type {lean}`Verso.Doc.Block genre` for some implicit {name}`genre`. -/
+  blocks : Array Term := #[]
+  /-- Syntax denoting values of type {lean}`genre.PartMetadata` for some implicit {name}`genre`. -/
+  partMetadata : Array Term := #[]
+  /-- Other modules referenced in this document by name -/
+  docs : NameSet := {}
+
+/--
+A {name}`FinishedPart` is the result of elaborating a document's part structure.
+-/
+public inductive FinishedPart where
+  | mk (titleSyntax : Syntax)
+       (expandedTitle : Array Term)
+       (titlePreview : String)
+       (metadata : Option Term)
+       (blocks : Array Term)
+       (subParts : Array FinishedPart)
+       (endPos : String.Pos.Raw)
+    /-- A name representing a Part-structured document in another module -/
+  | included (name : Ident)
+deriving Repr, BEq
+
+/--
+Transform a {name}`FinishedPart` into {name}`Json`, extracting any non-serializable data in the
+{name}`SerializableAux` data structure.
+-/
+public partial def FinishedPart.serialize [Monad m] [MonadRef m] [MonadQuotation m] : FinishedPart → StateT SerializableAux m Json
+  | .mk _titleSyntax title titlePreview metadata blocks subParts _endPos => do
+    let aux ← get
+    let titleJson := title.mapIdx (fun n _ => .num <| n + aux.inlines.size)
+    let contentJson := blocks.mapIdx (fun n _ => .num <| n + aux.blocks.size)
+    set ({ aux with
+      inlines := aux.inlines ++ title
+      blocks := aux.blocks ++ blocks })
+
+    let aux ← get
+    let metadataJson ← match metadata with
+      | .none => pure Json.null
+      | .some s =>
+        let n := aux.partMetadata.size
+        set { aux with partMetadata := aux.partMetadata.push s }
+        pure <| Json.arr #[.num n]
+
+    let subPartsJson ← subParts.mapM serialize
+
+    return .mkObj [
+      ("title", .arr titleJson),
+      ("titleString", .str titlePreview),
+      ("metadata", metadataJson),
+      ("content", .arr contentJson),
+      ("subParts", .arr subPartsJson),
+    ]
+
+  | .included name => do
+    modify (fun aux => { aux with docs := aux.docs.insert name.getId })
+    -- NB: deserialization depends on the implementation-defined behavior
+    -- that this will be a string
+    return ToJson.toJson name.getId