Renaming

Author: robsimmons

src/tests/Tests/Basic.lean

@@ -276,3 +276,4 @@ info: Verso.Doc.Part.mk
 #### Sub^3section
 
 :::::::
+

src/tests/Tests/Elab.lean

@@ -75,4 +75,3 @@ A variable like {lean}`(_ : Nat)`.
 :::::::
 A variable like {lean}`_`.
 :::::::
-

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

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

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
 

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

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