refactor: rename VersoDoc to DocThunk

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,

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

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

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

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'

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

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

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
@@ -247,7 +248,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 +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 VersoDoc.mk (fun _ => p) "{}"
+  return DocThunk.value p
 where
   docstringBlock (doc : LitVersoDocString) : Array (Block g) :=
     let parts := doc.subsections.map loadPart

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

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,

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
@@ -659,55 +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.

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
@@ -85,7 +86,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 +98,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 +216,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

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
 
@@ -21,7 +22,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 +42,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 =>