diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 8a53c8fd48..259331a08b 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -145,6 +145,9 @@ instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (Excep
   restoreM x := x
 
 class MonadFinally (m : Type u → Type v) where
+  /-- `tryFinally' x f` runs `x` to get `a : α` and then the finally function `f (some a)`.
+  If `x` fails for `m`'s definition of failure, it will run `f none`.
+  Hence it can be thought of as performing the same role as a `finally` block in an imperative programming language.-/
   tryFinally' {α β} : m α → (Option α → m β) → m (α × β)
 
 export MonadFinally (tryFinally')
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index e54d0efa28..07c0d6a452 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -15,7 +15,7 @@ namespace Lean.Elab
 
 open Std (PersistentArray PersistentArray.empty PersistentHashMap)
 
-/- Context after executing `liftTermElabM`.
+/-- Context after executing `liftTermElabM`.
    Note that the term information collected during elaboration may contain metavariables, and their
    assignments are stored at `mctx`. -/
 structure ContextInfo where
@@ -70,9 +70,11 @@ structure FieldInfo where
   stx       : Syntax
   deriving Inhabited
 
-/- We store the list of goals before and after the execution of a tactic.
-   We also store the metavariable context at each time since, we want to unassigned metavariables
-   at tactic execution time to be displayed as `?m...`. -/
+/-- The information needed to render the tactic state in the infoview.
+
+    We store the list of goals before and after the execution of a tactic.
+    We also store the metavariable context at each time since, we want to unassigned metavariables
+    at tactic execution time to be displayed as `?m...`. -/
 structure TacticInfo extends ElabInfo where
   mctxBefore  : MetavarContext
   goalsBefore : List MVarId
@@ -96,6 +98,7 @@ def CustomInfo.format : CustomInfo → Format
 
 instance : ToFormat CustomInfo := ⟨CustomInfo.format⟩
 
+/-- Header information for a node in `InfoTree`. -/
 inductive Info where
   | ofTacticInfo (i : TacticInfo)
   | ofTermInfo (i : TermInfo)
@@ -106,10 +109,36 @@ inductive Info where
   | ofCustomInfo (i : CustomInfo)
   deriving Inhabited
 
+/-- The InfoTree is a structure that is generated during elaboration that is used
+    by the language server to look up information about objects at particular points
+    in the Lean document. For example, tactic information and expected type information in
+    the infoview and information about completions.
+
+    The infotree consists of nodes which may have child nodes. Each node
+    has an `Info` object that contains details about what kind of information
+    is present. Each `Info` object also contains a `Syntax` instance, this is used to
+    map positions in the Lean document to particular info objects.
+
+    An example of a function that extracts information from an infotree for a given
+    position is `InfoTree.goalsAt?` which finds `TacticInfo`.
+
+    Information concerning expressions requires that a context also be saved,
+    `context` nodes store a local context that are used to properly the expressions
+    in lower nodes.
+
+    Because the info tree is generated during elaboration, some parts of the infotree
+    for a particular piece of syntax may not be ready yet. Hence InfoTree supports metavariable-like
+    `hole`s which are filled in later in the same way that unassigned metavariables are.
+-/
 inductive InfoTree where
-  | context (i : ContextInfo) (t : InfoTree) -- The context object is created by `liftTermElabM` at `Command.lean`
-  | node (i : Info) (children : PersistentArray InfoTree) -- The children contains information for nested term elaboration and tactic evaluation
-  | hole (mvarId : MVarId) -- The elaborator creates holes (aka metavariables) for tactics and postponed terms
+  | /-- The context object is created by `liftTermElabM` at `Command.lean` -/
+    context (i : ContextInfo) (t : InfoTree)
+  | /-- The children contains information for nested term elaboration and tactic evaluation -/
+    node (i : Info) (children : PersistentArray InfoTree)
+  | /-- For user data. -/
+    ofJson (j : Json)
+  | /-- The elaborator creates holes (aka metavariables) for tactics and postponed terms -/
+    hole (mvarId : MVarId)
   deriving Inhabited
 
 partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info :=
@@ -122,9 +151,22 @@ partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info
       ts.findSome? (findInfo? p)
   | _ => none
 
+/-- This structure is the state that is being used to build an InfoTree object.
+During elaboration, some parts of the info tree may be `holes` which need to be filled later.
+The `assignments` field is used to assign these holes.
+The `trees` field is a list of pending child trees. For the current infotree node that is being built.
+
+You should not need to use InfoState directly, instead infotrees should be built with the help of the methods here
+such as `pushInfoLeaf` to create leaf nodes and `withInfoContext` to create a nested child node.
+
+To see how `trees` is used, look at the function body of `withInfoContext'`.
+-/
 structure InfoState where
-  enabled    : Bool := false -- whether info trees should be recorded
-  assignment : PersistentHashMap MVarId InfoTree := {} -- map from holeId to InfoTree
+  /-- Whether info trees should be recorded. -/
+  enabled    : Bool := false
+  /-- Map from holes in the infotree to child infotrees. -/
+  assignment : PersistentHashMap MVarId InfoTree := {}
+  /-- Pending child trees of a node. -/
   trees      : PersistentArray InfoTree := {}
   deriving Inhabited
 
@@ -138,6 +180,8 @@ instance [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where
   getInfoState      := liftM (getInfoState : m _)
   modifyInfoState f := liftM (modifyInfoState f : m _)
 
+/-- Instantiate the holes on the given `tree` with the assignment table.
+(analoguous to instantiating the metavariables in an expression) -/
 partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMap MVarId InfoTree) : InfoTree :=
   match tree with
   | node i c => node i <| c.map (substitute · assignment)
@@ -272,6 +316,7 @@ variable [Monad m] [MonadInfoTree m]
 @[inline] private def modifyInfoTrees (f : PersistentArray InfoTree → PersistentArray InfoTree) : m Unit :=
   modifyInfoState fun s => { s with trees := f s.trees }
 
+/-- Returns the current array of InfoTrees and resets it to an empty array. -/
 def getResetInfoTrees : m (PersistentArray InfoTree) := do
   let trees := (← getInfoState).trees
   modifyInfoTrees fun _ => {}
@@ -288,6 +333,10 @@ def pushInfoLeaf (t : Info) : m Unit := do
 def addCompletionInfo (info : CompletionInfo) : m Unit := do
   pushInfoLeaf <| Info.ofCompletionInfo info
 
+/-- This does the same job as resolveGlobalConstNoOverload; resolving an identifier
+syntax to a unique fully resolved name or throwing if there are ambiguities.
+But also adds this reolved name to the infotree, this means that when you hover
+over a name in the sourcefile you will see the fully resolved name in the hover info.-/
 def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) (expectedType? : Option Expr := none) : m Name := do
   let n ← resolveGlobalConstNoOverload id
   if (← getInfoState).enabled then
@@ -295,6 +344,7 @@ def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [Mona
     pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := id, expectedType? }
   return n
 
+/-- Similar to resolveGlobalConstNoOverloadWithInfo, except if there are multiple name resolutions then it returns them as a list. -/
 def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) (expectedType? : Option Expr := none) : m (List Name) := do
   let ns ← resolveGlobalConst id
   if (← getInfoState).enabled then
@@ -302,6 +352,12 @@ def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
       pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := id, expectedType? }
   return ns
 
+/-- Use this to descend a node on the infotree that is being built.
+
+It saves the current list of trees `t₀` and resets it and then runs `x >>= mkInfo`, producing either an `i : Info` or a hole id.
+Running `x >>= mkInfo` will modify the trees state and produce a new list of trees `t₁`.
+In the `i : Info` case, `t₁` become the children of a node `node i t₁` that is appended to `t₀`.
+ -/
 def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MVarId)) : m α := do
   if (← getInfoState).enabled then
     let treesSaved ← getResetInfoTrees
@@ -317,6 +373,8 @@ def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MV
   else
     x
 
+/-- Saves the current list of trees `t₀`, runs `x` to produce a new tree list `t₁` and
+runs `mkInfoTree t₁` to get `n : InfoTree` and then restores the trees to be `t₀ ++ [n]`.-/
 def withInfoTreeContext [MonadFinally m] (x : m α) (mkInfoTree : PersistentArray InfoTree → m InfoTree) : m α := do
   if (← getInfoState).enabled then
     let treesSaved ← getResetInfoTrees
@@ -327,9 +385,13 @@ def withInfoTreeContext [MonadFinally m] (x : m α) (mkInfoTree : PersistentArra
   else
     x
 
+/-- Run `x` as a new child infotree node with header given by `mkInfo`. -/
 @[inline] def withInfoContext [MonadFinally m] (x : m α) (mkInfo : m Info) : m α := do
   withInfoTreeContext x (fun trees => do return InfoTree.node (← mkInfo) trees)
 
+/-- Resets the trees state `t₀`, runs `x` to produce a new trees
+state `t₁` and sets the state to be `t₀ ++ (InfoTree.context Γ <$> t₁)`
+where `Γ` is the context derived from the monad state. -/
 def withSaveInfoContext [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCtx m] [MonadResolveName m] [MonadFileMap m] (x : m α) : m α := do
   if (← getInfoState).enabled then
     let treesSaved ← getResetInfoTrees
@@ -338,7 +400,12 @@ def withSaveInfoContext [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCt
       let trees ← st.trees.mapM fun tree => do
         let tree := tree.substitute st.assignment
         pure <| InfoTree.context {
-          env := (← getEnv), fileMap := (← getFileMap), mctx := (← getMCtx), currNamespace := (← getCurrNamespace), openDecls := (← getOpenDecls), options := (← getOptions)
+          env := (← getEnv),
+          fileMap := (← getFileMap),
+          mctx := (← getMCtx),
+          currNamespace := (← getCurrNamespace),
+          openDecls := (← getOpenDecls),
+          options := (← getOptions)
         } tree
       modifyInfoTrees fun _ => treesSaved ++ trees
   else