From 96f2e3967ebeebfcb4a51be312466d3c991c593b Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 09:54:28 -0500
Subject: [PATCH 1/4] refactor: rename VersoDoc to DocThunk

---
 src/tests/TestMain.lean                       |  4 +-
 src/tests/Tests/Basic.lean                    | 17 ++++---
 src/tests/Tests/GenericCode.lean              |  6 +--
 src/tests/Tests/LeanCode.lean                 |  2 +-
 src/tests/Tests/Refs.lean                     | 16 +++----
 .../VersoBlog/LiterateLeanPage.lean           |  4 +-
 .../VersoBlog/LiterateModuleDocs.lean         |  4 +-
 .../VersoLiterate/Exported.lean               |  4 +-
 src/verso-literate/VersoLiterate/Module.lean  |  2 +-
 src/verso-manual/VersoManual/Literate.lean    |  2 +-
 src/verso/Verso/Doc.lean                      | 48 +++++++++----------
 src/verso/Verso/Doc/Concrete.lean             |  8 ++--
 src/verso/Verso/Doc/Elab/Basic.lean           |  4 +-
 src/verso/Verso/Doc/Elab/Monad.lean           |  8 ++--
 src/verso/Verso/Doc/Name.lean                 |  6 +--
 15 files changed, 67 insertions(+), 68 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 597aef80..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
 
 
 /- ----- -/
@@ -276,4 +276,3 @@ info: Verso.Doc.Part.mk
 #### Sub^3section
 
 :::::::
-
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..8266cdd8 100644
--- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean
+++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean
@@ -528,8 +528,8 @@ def elabLiteratePage (x : Ident) (path : StrLit) (mod : Ident) (config : LitPage
       | _ => p
     else finished
 
-  let ty ← ``(VersoDoc $genre)
-  let doc ← Command.runTermElabM fun _ => finished.toVersoDoc genre ctx docState partState
+  let ty ← ``(DocThunk $genre)
+  let doc ← Command.runTermElabM fun _ => finished.toThunkTerm genre ctx docState partState
   elabCommand <| ← `(def $x : $ty := $doc)
 
 end Literate
diff --git a/src/verso-blog/VersoBlog/LiterateModuleDocs.lean b/src/verso-blog/VersoBlog/LiterateModuleDocs.lean
index 90973e73..e766e95a 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,
@@ -89,7 +89,7 @@ def elabFromModuleDocs (x : Ident) (path : StrLit) (mod : Ident) (title : StrLit
     pure name
 
   let metadata ← if let some m := metadata? then `(some $m) else `(none)
-  elabCommand <| ← `(command|def $x : VersoDoc $genre := $(mkIdent mod).withMetadata $metadata)
+  elabCommand <| ← `(command|def $x : DocThunk $genre := $(mkIdent mod).withMetadata $metadata)
 
 
 end
diff --git a/src/verso-literate/VersoLiterate/Exported.lean b/src/verso-literate/VersoLiterate/Exported.lean
index 7834a3c0..374a4380 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.mk (fun _ => p) "{}"
+  return DocThunk.mk (fun _ => 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.lean b/src/verso/Verso/Doc.lean
index df05f6b4..28ccd456 100644
--- a/src/verso/Verso/Doc.lean
+++ b/src/verso/Verso/Doc.lean
@@ -12,13 +12,6 @@ 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
@@ -665,28 +658,28 @@ public structure DocReconstruction where
 
 /--
 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`
+{name}`DocThunk` represents a not-fully-evaluated document of type {lean}`Part` that can be turned
+into a value by invoking the `DocThunk.force` method. The actual structure of a {name}`DocThunk`
 should not be relied on.
 -/
-public structure VersoDoc (genre : Genre) where
+public structure DocThunk (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) "{}"
+instance : Inhabited (DocThunk genre) where
+  default := DocThunk.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`.
+A {name}`DocThunk` represents a potentially-not-fully-evaluated {name}`Part`. Calling
+{name}`DocThunk.force` forces evaluation of the {name}`DocThunk` to a {name}`Part`.
 -/
-public def VersoDoc.toPart: VersoDoc genre → Part genre
+public def DocThunk.force: DocThunk 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}"
+    | .error e => panic! s!"Failed to parse DocThunk's Export data as JSON: {e}"
     | .ok json =>
       if let .ok highlightJson := json.getObjVal? "highlight" then
         match SubVerso.Highlighting.Export.fromJson? highlightJson with
@@ -694,21 +687,26 @@ public def VersoDoc.toPart: VersoDoc genre → Part genre
         | .ok table => construct ⟨table⟩
       else construct ⟨{}⟩
 
+@[deprecated DocThunk (since := "2025-12-28")]
+public def VersoDoc : Genre → Type := DocThunk
+
+@[deprecated DocThunk.force (since := "2025-12-28")]
+public def VersoDoc.force : DocThunk genre → Part genre := DocThunk.force
+
+@[deprecated DocThunk.force (since := "2025-12-28")]
+public def VersoDoc.toPart : DocThunk genre → Part genre := DocThunk.force
+
+@[deprecated DocThunk.force (since := "2025-12-28")]
+public def DocThunk.toPart : DocThunk genre → Part genre := DocThunk.force
+
 /--
-Replace the metadata in a VersoDoc.
+Replace the metadata in a {name}`DocThunk`.
 
 This is something of a hack used as a workaround in LiterateModuleDocs.
 -/
-public def VersoDoc.withMetadata (metadata? : Option genre.PartMetadata)  : VersoDoc genre → VersoDoc genre
+public def DocThunk.withMetadata (metadata? : Option genre.PartMetadata)  : DocThunk genre → DocThunk 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/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
index a8594e95..b2c4c6aa 100644
--- a/src/verso/Verso/Doc/Concrete.lean
+++ b/src/verso/Verso/Doc/Concrete.lean
@@ -85,7 +85,7 @@ private meta def elabDoc (genre: Term) (title: StrLit) (topLevelBlocks : Array S
   let finished := partElabState.partContext.toPartFrame.close endPos
 
   pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC}
-  finished.toVersoDoc genre ctx docElabState partElabState
+  finished.toThunkTerm genre ctx docElabState partElabState
 
 elab "#docs" "(" genre:term ")" n:ident title:str ":=" ":::::::" text:document ":::::::" : command => do
   findGenreCmd genre
@@ -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
@@ -215,8 +215,8 @@ private meta def finishDoc (genreSyntax : Term) (title : StrLit) : Command.Comma
   let finished := versoEnv.partState.partContext.toPartFrame.close endPos
 
   let n := mkIdentFrom title (← currentDocName)
-  let doc ← Command.runTermElabM fun _ => finished.toVersoDoc genreSyntax versoEnv.ctx versoEnv.docState versoEnv.partState
-  let ty ← ``(VersoDoc $genreSyntax)
+  let doc ← Command.runTermElabM fun _ => finished.toThunkTerm genreSyntax versoEnv.ctx versoEnv.docState versoEnv.partState
+  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 4fe20620..68f95536 100644
--- a/src/verso/Verso/Doc/Elab/Basic.lean
+++ b/src/verso/Verso/Doc/Elab/Basic.lean
@@ -21,7 +21,7 @@ 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` -/
+    /-- A name representing a value of type {lean}`DocThunk` -/
   | included (name : Ident)
 deriving Repr, BEq
 
@@ -41,7 +41,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 831645e7..c6daa619 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -463,10 +463,10 @@ unsafe def inlineExpandersForUnsafe (x : Name) : DocElabM (Array InlineExpander)
 public opaque inlineExpandersFor (x : Name) : DocElabM (Array InlineExpander)
 
 /--
-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
+public def FinishedPart.toThunkTerm
     (genreSyntax : Term)
     (finished : FinishedPart)
     (ctx : DocElabContext)
@@ -532,8 +532,10 @@ public def FinishedPart.toVersoDoc
     | .none => Json.mkObj []
     | .some table => Json.mkObj [("highlight", table.toExport.toJson)]
 
-  ``(VersoDoc.mk (fun $docReconstructionPlaceholder => $finishedSyntax) $(quote reconstJson.compress))
+  ``(DocThunk.mk (fun $docReconstructionPlaceholder => $finishedSyntax) $(quote reconstJson.compress))
 
+@[deprecated FinishedPart.toThunkTerm (since := "2025-11-28")]
+public def FinishedPart.toVersoDoc : Term → FinishedPart → DocElabContext → DocElabM.State → PartElabM.State → TermElabM Term := FinishedPart.toThunkTerm
 
 public abbrev BlockExpander := Syntax → DocElabM (TSyntax `term)
 
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

From 41cc5c326e5651c0df5618fde11eada549fa6581 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 12:12:17 -0500
Subject: [PATCH 2/4] move DocThunk to Verso.Doc.Reconstruct

---
 .../VersoLiterate/Exported.lean               |  3 +-
 src/verso/Verso/Doc.lean                      | 54 ------------
 src/verso/Verso/Doc/Concrete.lean             |  1 +
 src/verso/Verso/Doc/Elab/Basic.lean           |  1 +
 src/verso/Verso/Doc/Elab/Monad.lean           |  3 +-
 src/verso/Verso/Doc/Reconstruct.lean          | 84 +++++++++++++++++++
 6 files changed, 90 insertions(+), 56 deletions(-)
 create mode 100644 src/verso/Verso/Doc/Reconstruct.lean

diff --git a/src/verso-literate/VersoLiterate/Exported.lean b/src/verso-literate/VersoLiterate/Exported.lean
index 374a4380..de7aa0a1 100644
--- a/src/verso-literate/VersoLiterate/Exported.lean
+++ b/src/verso-literate/VersoLiterate/Exported.lean
@@ -7,6 +7,7 @@ Author: David Thrane Christiansen
 import Lean.Data.Json
 import Lean.DocString.Extension
 import Verso.Doc
+import Verso.Doc.Reconstruct
 import SubVerso.Highlighting
 import SubVerso.Module
 import VersoLiterate.Basic
@@ -305,7 +306,7 @@ partial def modToPage [LoadLiterate g] (mod : LitMod) (title : Array (Inline g))
     let p' := stack.back
     stack := stack.pop
     p := pushPart p' p
-  return DocThunk.mk (fun _ => p) "{}"
+  return DocThunk.value 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 28ccd456..846b75ec 100644
--- a/src/verso/Verso/Doc.lean
+++ b/src/verso/Verso/Doc.lean
@@ -652,60 +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
-{name}`DocThunk` represents a not-fully-evaluated document of type {lean}`Part` that can be turned
-into a value by invoking the `DocThunk.force` method. The actual structure of a {name}`DocThunk`
-should not be relied on.
--/
-public structure DocThunk (genre : Genre) where
-  construct : DocReconstruction → Part genre
-
-  /-- Serialization of the DocReconstruction data structure -/
-  docReconstructionData : String := "{}"
-
-instance : Inhabited (DocThunk genre) where
-  default := DocThunk.mk (fun _ => Inhabited.default) "{}"
-
-
-/--
-A {name}`DocThunk` represents a potentially-not-fully-evaluated {name}`Part`. Calling
-{name}`DocThunk.force` forces evaluation of the {name}`DocThunk` to a {name}`Part`.
--/
-public def DocThunk.force: DocThunk genre → Part genre
-  | .mk construct highlight =>
-    match Json.parse highlight with
-    | .error e => panic! s!"Failed to parse DocThunk'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 ⟨{}⟩
-
-@[deprecated DocThunk (since := "2025-12-28")]
-public def VersoDoc : Genre → Type := DocThunk
-
-@[deprecated DocThunk.force (since := "2025-12-28")]
-public def VersoDoc.force : DocThunk genre → Part genre := DocThunk.force
-
-@[deprecated DocThunk.force (since := "2025-12-28")]
-public def VersoDoc.toPart : DocThunk genre → Part genre := DocThunk.force
-
-@[deprecated DocThunk.force (since := "2025-12-28")]
-public def DocThunk.toPart : DocThunk genre → Part genre := DocThunk.force
-
-/--
-Replace the metadata in a {name}`DocThunk`.
-
-This is something of a hack used as a workaround in LiterateModuleDocs.
--/
-public def DocThunk.withMetadata (metadata? : Option genre.PartMetadata)  : DocThunk genre → DocThunk genre
-  | .mk construct docReconstStr => .mk (fun docReconst => { construct docReconst with metadata := metadata? }) docReconstStr
 
 /--
 Specifies how to modify the context while traversing the contents of a given part.
diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
index b2c4c6aa..2fefa1f1 100644
--- a/src/verso/Verso/Doc/Concrete.lean
+++ b/src/verso/Verso/Doc/Concrete.lean
@@ -9,6 +9,7 @@ public meta import Verso.Parser
 public import Lean.Elab.Command
 public meta import SubVerso.Highlighting.Export
 import Verso.Doc
+import Verso.Doc.Reconstruct
 public import Verso.Doc.Elab
 public meta import Verso.Doc.Elab.Monad
 import Verso.Doc.Concrete.InlineString
diff --git a/src/verso/Verso/Doc/Elab/Basic.lean b/src/verso/Verso/Doc/Elab/Basic.lean
index 68f95536..5e5e9a14 100644
--- a/src/verso/Verso/Doc/Elab/Basic.lean
+++ b/src/verso/Verso/Doc/Elab/Basic.lean
@@ -5,6 +5,7 @@ Author: David Thrane Christiansen, Rob Simmons
 -/
 module
 public import Verso.Doc
+import Verso.Doc.Reconstruct
 
 open Lean
 
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index c6daa619..9b40c6cf 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -14,6 +14,7 @@ import Lean.DocString
 
 import SubVerso.Highlighting
 import Verso.Doc
+import Verso.Doc.Reconstruct
 public import Verso.Doc.ArgParse
 public import Verso.Doc.Elab.InlineString
 meta import Verso.Doc.Elab.InlineString
@@ -532,7 +533,7 @@ public def FinishedPart.toThunkTerm
     | .none => Json.mkObj []
     | .some table => Json.mkObj [("highlight", table.toExport.toJson)]
 
-  ``(DocThunk.mk (fun $docReconstructionPlaceholder => $finishedSyntax) $(quote reconstJson.compress))
+  ``(DocThunk.serialized (fun $docReconstructionPlaceholder => $finishedSyntax) $(quote reconstJson.compress) none)
 
 @[deprecated FinishedPart.toThunkTerm (since := "2025-11-28")]
 public def FinishedPart.toVersoDoc : Term → FinishedPart → DocElabContext → DocElabM.State → PartElabM.State → TermElabM Term := FinishedPart.toThunkTerm
diff --git a/src/verso/Verso/Doc/Reconstruct.lean b/src/verso/Verso/Doc/Reconstruct.lean
new file mode 100644
index 00000000..b3bf5033
--- /dev/null
+++ b/src/verso/Verso/Doc/Reconstruct.lean
@@ -0,0 +1,84 @@
+/-
+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 SubVerso.Highlighting
+public import Verso.Doc
+
+set_option doc.verso true
+set_option pp.rawOnError true
+
+namespace Verso.Doc
+open Lean
+
+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
+{name}`DocThunk` represents a partially-serialized document of type {lean}`Part` that can be turned
+into a value by invoking the `DocThunk.force` method. The internal structure of a {name}`DocThunk`
+should not be relied upon.
+-/
+public inductive DocThunk (genre : Genre) where
+  /--
+  A partially-serialized document. If the {name}`replacementMetadata?` is non-{name}`none`, the
+  value will replace the outermost {name}`Part.metadata` field of the reconstructed document.
+  -/
+  | serialized
+      (construct : DocReconstruction → Part genre)
+      (docReconstructionData : String := "{}")
+      (replacementMetadata? : Option (Option genre.PartMetadata))
+
+  /--
+  For pathways that build {lean}`Part` values directly, there is no value in, or need for, a
+  serialization phase.
+  -/
+  | value (part : Part genre)
+
+instance : Inhabited (DocThunk genre) where
+  default := .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 construct docReconstStr _ =>
+    .serialized construct docReconstStr (.some metadata?)
+  | .value part =>
+    .value { part with metadata := metadata? }
+
+/--
+A {name}`DocThunk` represents a potentially-not-fully-evaluated {name}`Part`. Calling
+{name}`DocThunk.force` forces evaluation of the {name}`DocThunk` to a {name}`Part`.
+-/
+public def DocThunk.force: DocThunk genre → Part genre
+  | .serialized construct highlight metadata? =>
+    match Json.parse highlight with
+    | .error e => panic! s!"Failed to parse DocThunk's Export data as JSON: {e}"
+    | .ok json =>
+      let part :=
+        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 ⟨{}⟩
+      match metadata? with
+      | .none => part
+      | .some replacement => { part with metadata := replacement }
+  | .value part => part
+
+@[deprecated DocThunk (since := "2025-12-28")]
+public def VersoDoc : Genre → Type := DocThunk
+
+@[deprecated DocThunk.force (since := "2025-12-28")]
+public def VersoDoc.force : DocThunk genre → Part genre := DocThunk.force
+
+@[deprecated DocThunk.force (since := "2025-12-28")]
+public def VersoDoc.toPart : DocThunk genre → Part genre := DocThunk.force
+
+@[deprecated DocThunk.force (since := "2025-12-28")]
+public def DocThunk.toPart : DocThunk genre → Part genre := DocThunk.force

From 81289cacb071683ccdedda6a84a9560410334863 Mon Sep 17 00:00:00 2001
From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com>
Date: Mon, 5 Jan 2026 10:26:55 -0500
Subject: [PATCH 3/4] Update src/verso/Verso/Doc/Reconstruct.lean

Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
---
 src/verso/Verso/Doc/Reconstruct.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/verso/Verso/Doc/Reconstruct.lean b/src/verso/Verso/Doc/Reconstruct.lean
index b3bf5033..6658b505 100644
--- a/src/verso/Verso/Doc/Reconstruct.lean
+++ b/src/verso/Verso/Doc/Reconstruct.lean
@@ -43,7 +43,7 @@ instance : Inhabited (DocThunk genre) where
   default := .value default
 
 /--
-Replace the top-level metadata in a {name}`DocThunk` without forcing the thunk.
+Replaces 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 construct docReconstStr _ =>

From d076d396a7b5080e4851e2e3c6c1d5e36526450c Mon Sep 17 00:00:00 2001
From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com>
Date: Mon, 5 Jan 2026 10:27:04 -0500
Subject: [PATCH 4/4] Update src/verso/Verso/Doc/Reconstruct.lean

Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
---
 src/verso/Verso/Doc/Reconstruct.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/verso/Verso/Doc/Reconstruct.lean b/src/verso/Verso/Doc/Reconstruct.lean
index 6658b505..6d23547c 100644
--- a/src/verso/Verso/Doc/Reconstruct.lean
+++ b/src/verso/Verso/Doc/Reconstruct.lean
@@ -55,7 +55,7 @@ public def DocThunk.withMetadata (metadata? : Option genre.PartMetadata)  : DocT
 A {name}`DocThunk` represents a potentially-not-fully-evaluated {name}`Part`. Calling
 {name}`DocThunk.force` forces evaluation of the {name}`DocThunk` to a {name}`Part`.
 -/
-public def DocThunk.force: DocThunk genre → Part genre
+public def DocThunk.force : DocThunk genre → Part genre
   | .serialized construct highlight metadata? =>
     match Json.parse highlight with
     | .error e => panic! s!"Failed to parse DocThunk's Export data as JSON: {e}"