diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
index 81575ed3..24835a8e 100644
--- a/REPL/Frontend.lean
+++ b/REPL/Frontend.lean
@@ -4,11 +4,44 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean.Elab.Frontend
+import Std.Data.HashMap
 
-open Lean Elab
+open Lean Elab Language
 
 namespace Lean.Elab.IO
 
+partial def IO.processCommandsIncrementally' (inputCtx : Parser.InputContext)
+    (parserState : Parser.ModuleParserState) (commandState : Command.State)
+    (old? : Option IncrementalState) :
+    BaseIO (List (IncrementalState × Option InfoTree)) := do
+  let task ← Language.Lean.processCommands inputCtx parserState commandState
+    (old?.map fun old => (old.inputCtx, old.initialSnap))
+  return go task.get task #[]
+where
+  go initialSnap t commands :=
+    let snap := t.get
+    let commands := commands.push snap
+    -- Opting into reuse also enables incremental reporting, so make sure to collect messages from
+    -- all snapshots
+    let messages := toSnapshotTree initialSnap
+      |>.getAll.map (·.diagnostics.msgLog)
+      |>.foldl (· ++ ·) {}
+    -- In contrast to messages, we should collect info trees only from the top-level command
+    -- snapshots as they subsume any info trees reported incrementally by their children.
+    let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray'
+    let result : (IncrementalState × Option InfoTree) :=
+      ({ commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees }
+         , parserState := snap.parserState
+         , cmdPos := snap.parserState.pos
+         , commands := commands.map (·.stx)
+         , inputCtx := inputCtx
+         , initialSnap := initialSnap
+       }, snap.infoTreeSnap.get.infoTree?)
+    if let some next := snap.nextCmdSnap? then
+      result :: go initialSnap next.task commands
+    else
+      [result]
+
 /--
 Wrapper for `IO.processCommands` that enables info states, and returns
 * the new command state
@@ -17,41 +50,48 @@ Wrapper for `IO.processCommands` that enables info states, and returns
 -/
 def processCommandsWithInfoTrees
     (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
-    (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
+    (commandState : Command.State) (incrementalState? : Option IncrementalState := none)
+    : IO (List (IncrementalState × Option InfoTree) × List Message) := do
   let commandState := { commandState with infoState.enabled := true }
-  let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  pure (s, s.messages.toList, s.infoState.trees.toList)
+  let incStates ← IO.processCommandsIncrementally' inputCtx parserState commandState incrementalState?
+  pure (incStates, (incStates.getLast?.map (·.1.commandState.messages.toList)).getD {})
 
 /--
 Process some text input, with or without an existing command state.
-If there is no existing environment, we parse the input for headers (e.g. import statements),
-and create a new environment.
-Otherwise, we add to the existing environment.
+Supports header caching to avoid reprocessing the same imports repeatedly.
 
 Returns:
-1. The header-only command state (only useful when cmdState? is none)
-2. The resulting command state after processing the entire input
-3. List of messages
-4. List of info trees
+1. The resulting command state after processing the entire input
+2. List of messages
+3. List of info trees along with Command.State from the incremental processing
+4. Updated header cache mapping import keys to Command.State
 -/
 def processInput (input : String) (cmdState? : Option Command.State)
+    (incrementalState? : Option IncrementalState := none)
+    (headerCache : Std.HashMap String Command.State)
     (opts : Options := {}) (fileName : Option String := none) :
-    IO (Command.State × Command.State × List Message × List InfoTree) := unsafe do
+    IO (Command.State × List (IncrementalState × Option InfoTree) × List Message × (Std.HashMap String Command.State)) := unsafe do
   Lean.initSearchPath (← Lean.findSysroot)
   enableInitializersExecution
   let fileName   := fileName.getD "<input>"
   let inputCtx   := Parser.mkInputContext input fileName
-
   match cmdState? with
   | none => do
-    -- Split the processing into two phases to prevent self-reference in proofs in tactic mode
     let (header, parserState, messages) ← Parser.parseHeader inputCtx
-    let (env, messages) ← processHeader header opts messages inputCtx
-    let headerOnlyState := Command.mkState env messages opts
-    let (cmdState, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState
-    return (headerOnlyState, cmdState, messages, trees)
-
+    let importKey := (input.take parserState.pos.byteIdx).trim
+    match headerCache.get? importKey with
+    | some cachedHeaderState => do
+      -- Header is cached, use it as the base command state
+      let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState cachedHeaderState incrementalState?
+      return (cachedHeaderState, incStates, messages, headerCache)
+    | none => do
+      -- Header not cached, process it and cache the result
+      let (env, messages) ← processHeader header opts messages inputCtx
+      let headerOnlyState := Command.mkState env messages opts
+      let headerCache := headerCache.insert importKey headerOnlyState
+      let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState incrementalState?
+      return (headerOnlyState, incStates, messages, headerCache)
   | some cmdStateBefore => do
     let parserState : Parser.ModuleParserState := {}
-    let (cmdStateAfter, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore
-    return (cmdStateBefore, cmdStateAfter, messages, trees)
+    let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore incrementalState?
+    return (cmdStateBefore, incStates, messages, headerCache)
diff --git a/REPL/JSON.lean b/REPL/JSON.lean
index 24db8402..303384cd 100644
--- a/REPL/JSON.lean
+++ b/REPL/JSON.lean
@@ -13,7 +13,10 @@ namespace REPL
 
 structure CommandOptions where
   allTactics : Option Bool := none
+  declTypes: Option Bool := none
+  namespaces: Option Bool := none
   rootGoals : Option Bool := none
+  conclusions : Option Bool := none
   /--
   Should be "full", "tactics", "original", or "substantive".
   Anything else is ignored.
@@ -46,7 +49,7 @@ deriving ToJson, FromJson
 structure Pos where
   line : Nat
   column : Nat
-deriving ToJson, FromJson
+deriving ToJson, FromJson, BEq, Hashable
 
 /-- Severity of a message. -/
 inductive Severity
@@ -116,6 +119,45 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState :
     proofState,
     usedConstants }
 
+structure DeclType where
+  pos : Pos
+  endPos : Pos
+  type : String
+  pp : String
+  conclusion : String
+deriving ToJson, FromJson
+
+/-- Construct the JSON representation of a Declaration type. -/
+def DeclType.of (type pp conclusion : String) (pos endPos : Lean.Position) : DeclType :=
+  { pos := ⟨pos.line, pos.column⟩,
+    endPos := ⟨endPos.line, endPos.column⟩,
+    type,
+    pp
+    conclusion }
+
+structure Namespace where
+  pos : Pos
+  endPos : Pos
+  currentNamespace : String
+  openDecls: List String
+  pp : String
+deriving ToJson, FromJson
+
+def Namespace.of (currentNamespace pp : String) (openDecls : List String) (pos endPos : Lean.Position) : Namespace :=
+  { pos := ⟨pos.line, pos.column⟩,
+    endPos := ⟨endPos.line, endPos.column⟩,
+    currentNamespace,
+    openDecls,
+    pp }
+structure Conclusion where
+  pos : Pos
+  endPos : Pos
+  pp: String
+deriving FromJson, ToJson
+
+def Conclusion.of (pp : String) (pos endPos : Lean.Position) : Conclusion :=
+  {pos := ⟨pos.line, pos.column⟩, endPos := ⟨endPos.line, endPos.column⟩, pp := pp}
+
 /--
 A response to a Lean command.
 `env` can be used in later calls, to build on the stored environment.
@@ -125,6 +167,9 @@ structure CommandResponse where
   messages : List Message := []
   sorries : List Sorry := []
   tactics : List Tactic := []
+  decls: List DeclType := []
+  namespaces: List Namespace := []
+  conclusions : List Conclusion := []
   infotree : Option Json := none
 deriving FromJson
 
@@ -138,6 +183,9 @@ instance : ToJson CommandResponse where
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "tactics" r.tactics,
+    Json.nonemptyList "decls" r.decls,
+    Json.nonemptyList "namespaces" r.namespaces,
+    Json.nonemptyList "conclusions" r.conclusions,
     match r.infotree with | some j => [("infotree", j)] | none => []
   ]
 
diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean
index 88da1b98..0ced074b 100644
--- a/REPL/Lean/InfoTree.lean
+++ b/REPL/Lean/InfoTree.lean
@@ -130,14 +130,17 @@ Keep `.node` nodes and `.hole` nodes satisfying predicates.
 
 Returns a `List InfoTree`, although in most situations this will be a singleton.
 -/
-partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
+partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) (stop: Info → Bool := fun _ => false) :
     InfoTree → List InfoTree
-  | .context ctx tree => tree.filter p m |>.map (.context ctx)
+  | .context ctx tree => tree.filter p m stop |>.map (.context ctx)
   | .node info children =>
     if p info then
-      [.node info (children.toList.map (filter p m)).flatten.toPArray']
+      if stop info then
+        [.node info children]
+      else
+        [.node info (children.toList.map (filter p m stop)).flatten.toPArray']
     else
-      (children.toList.map (filter p m)).flatten
+      if stop info then children.toList else (children.toList.map (filter p m stop)).flatten
   | .hole mvar => if m mvar then [.hole mvar] else []
 
 /-- Discard all nodes besides `.context` nodes and `TacticInfo` nodes. -/
@@ -190,6 +193,35 @@ def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo × List MVa
   | (.ofTacticInfo i, some ctx, rootGoals) => (i, ctx, rootGoals)
   | _ => none
 
+/-- Returns all `TermInfo` nodes for a given `InfoTree`. -/
+partial def findTermNodes (t : InfoTree) (ctx? : Option ContextInfo := none) :
+  List (TermInfo × ContextInfo) :=
+  let infoCtx := t.findAllInfo ctx? fun (info: Info) =>
+    match info with
+    | .ofTermInfo _ => true
+    | _ => false
+  infoCtx.flatMap fun ⟨info, ctx?⟩ =>
+   match info with
+   | .ofTermInfo i => match ctx? with
+    | some ctx => [(i, ctx)]
+    | _ => []
+   | _ => []
+
+
+/-- Returns all `CommandInfo` nodes for a given `InfoTree`. -/
+partial def findCommandNodes (t : InfoTree) (ctx? : Option ContextInfo := none) :
+  List (CommandInfo × ContextInfo) :=
+  let infoCtx := t.findAllInfo ctx? fun (info: Info) =>
+    match info with
+    | .ofCommandInfo _ => true
+    | _ => false
+  infoCtx.flatMap fun ⟨info, ctx?⟩ =>
+   match info with
+   | .ofCommandInfo i => match ctx? with
+    | some ctx => [(i, ctx)]
+    | _ => []
+   | _ => []
+
 /-- Returns the root goals for a given `InfoTree`. -/
 partial def findRootGoals (t : InfoTree) (ctx? : Option ContextInfo := none) :
   List (TacticInfo × ContextInfo × List MVarId) :=
@@ -258,6 +290,75 @@ def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × List
       range.snd,
       i.getUsedConstantsAsSet.toArray )
 
+def declType (t : InfoTree) : Option (ContextInfo × Expr × Syntax × LocalContext × Position × Position) :=
+  let terms: List (TermInfo × ContextInfo) := t.findTermNodes
+  match terms.getLast? with
+  | some ⟨i, ctx⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    (ctx, i.expr, i.stx, i.lctx, range.fst, range.snd)
+  | _ => none
+
+def namespaces (t : InfoTree) : List (CommandInfo × ContextInfo × Position × Position) :=
+  let nodes := t.findCommandNodes |>.filter fun ⟨i, _⟩ =>
+    match i.elaborator with
+    | ``Lean.Elab.Command.elabOpen => true
+    | ``Lean.Elab.Command.elabSection => true
+    | ``Lean.Elab.Command.elabEnd => true
+    | ``Lean.Elab.Command.elabNamespace => true
+    | _ => false
+  nodes.map fun ⟨i, ctx⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    (i, ctx, range.fst, range.snd)
+
+-- Get the TermInfo with the largest position in the file
+partial def maxTermNode (terms: List (TermInfo × Option ContextInfo)) : Option (TermInfo × ContextInfo) :=
+  match terms.head? with
+  | some ⟨ti, ctx?⟩ =>
+    let largestTail := maxTermNode terms.tail
+    match largestTail with
+    | some ⟨tailinfo, tailctx⟩ =>
+      match ctx? with
+      | some ctx =>
+        let range := stxRange ctx.fileMap ti.stx
+        let tailRange := stxRange tailctx.fileMap tailinfo.stx
+        if tailRange.snd.line > range.snd.line then some ⟨tailinfo, tailctx⟩
+        else
+          if tailRange.snd.column > range.snd.column then some ⟨tailinfo, tailctx⟩
+          else some ⟨ti, ctx⟩
+      | none => some ⟨tailinfo, tailctx⟩
+    | none => match ctx? with
+      | some ctx => some ⟨ti, ctx⟩
+      | none => none
+  | none => none
+
+def conclusion (t : InfoTree) : IO (List (TermInfo × ContextInfo)) := do
+  let only_declarations := fun i => match i with
+    | .ofCommandInfo m => if m.elaborator == ``Lean.Elab.Command.elabDeclaration then
+      match m.stx.getArgs.toList.getLast? with
+      | some stx => stx.getKind == ``Lean.Parser.Command.theorem
+      | none => false
+      else false
+    | _ => false
+  let only_term := fun i => match i with
+    | .ofTermInfo _ => true
+    | _ => false
+
+  let trees := t.filter (fun i => only_declarations i) (stop := only_declarations)
+  let terms_info : List (List (Info × Option ContextInfo)) := trees.map <| fun t => t.findAllInfo none only_term (stop := fun i => Bool.not <| only_declarations i)
+
+  let terms: List (List (TermInfo × Option ContextInfo)) := terms_info.map <| fun t => t.flatMap (fun ⟨i, ctx?⟩ =>
+    match i with
+    | .ofTermInfo ti => match ti.stx.getHeadInfo with
+      | .original .. => [⟨ti, ctx?⟩]
+      | _ => []
+    | _ => [])
+
+  let optional_conclusions := terms.map <| fun ts => maxTermNode ts
+  pure (optional_conclusions.flatMap <| fun c =>
+    match c with
+    | some s => [s]
+    | _ => [])
+
 def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) :=
   t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ =>
     let range := stxRange ctx.fileMap i.stx
diff --git a/REPL/Main.lean b/REPL/Main.lean
index b00b6833..4fbca112 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -11,6 +11,8 @@ import REPL.Lean.Environment
 import REPL.Lean.InfoTree
 import REPL.Lean.InfoTree.ToJson
 import REPL.Snapshots
+import Lean.Data.Trie
+import Std.Data.HashMap
 
 /-!
 # A REPL for Lean.
@@ -72,6 +74,16 @@ structure State where
   and report the numerical index for the recorded state at each sorry.
   -/
   proofStates : Array ProofSnapshot := #[]
+  /--
+  Trie-based storage for fast prefix matching, organized by environment ID.
+  Map from environment ID (None for fresh env) to trie of command prefixes with incremental states.
+  -/
+  envTries : Std.HashMap (Option Nat) (Lean.Data.Trie IncrementalState) := Std.HashMap.emptyWithCapacity 8
+  /--
+  Cache for processed headers (import statements) to avoid reprocessing the same imports repeatedly.
+  Maps import raw string to the processed command state.
+  -/
+  headerCache : Std.HashMap String Command.State := Std.HashMap.emptyWithCapacity 8
 
 /--
 The Lean REPL monad.
@@ -88,12 +100,43 @@ def recordCommandSnapshot (state : CommandSnapshot) : M m Nat := do
   modify fun s => { s with cmdStates := s.cmdStates.push state }
   return id
 
+/-- Add all incremental states of a command to the trie at their corresponding prefix positions -/
+def addCommandToTrie (cmdText : String)
+    (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do
+  let state ← get
+  let currentTrie := state.envTries.get? envId? |>.getD Lean.Data.Trie.empty
+
+  let mut newTrie := currentTrie
+  for (incState, _) in incStates do
+    let prefixPos := incState.cmdPos.byteIdx
+    let cmdPrefix : String := (cmdText.take prefixPos).trim
+    newTrie := newTrie.insert cmdPrefix incState
+
+  modify fun s => { s with envTries := s.envTries.insert envId? newTrie }
+
+/-- Record command text and incremental states for prefix matching reuse. -/
+def recordCommandIncrementals (cmdText : String)
+    (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do
+  addCommandToTrie cmdText incStates envId?
+
 /-- Record a `ProofSnapshot` into the REPL state, returning its index for future use. -/
 def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   let id := (← get).proofStates.size
   modify fun s => { s with proofStates := s.proofStates.push proofState }
   return id
 
+/-- Find the best incremental state using trie-based prefix matching -/
+def findBestIncrementalState (newCmd : String) (envId? : Option Nat) : M m (Option IncrementalState) := do
+  let state ← get
+  let trimmedCmd := newCmd.trim
+  let trie? := state.envTries.get? envId?
+  match trie? with
+  | none => return none
+  | some trie =>
+    match trie.matchPrefix trimmedCmd 0 with
+    | some incState => return some incState
+    | none => return none
+
 def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId))
 : M m (List Sorry) :=
   trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with
@@ -102,11 +145,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
       fun ⟨ctx, g, pos, endPos⟩ => do
         let (goal, proofState) ← match g with
         | .tactic g => do
-          let lctx ← ctx.runMetaM {} do
-              match ctx.mctx.findDecl? g with
-              | some decl => return decl.lctx
-              | none => throwError "unknown metavariable '{g}'"
-          let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals?
+          let s ← ProofSnapshot.create ctx none env? [g] rootGoals?
           pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term lctx (some t) => do
           let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t]
@@ -115,6 +154,16 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
         let proofStateId ← proofState.mapM recordProofSnapshot
         return Sorry.of goal pos endPos proofStateId
 
+def sorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment)
+(rootGoals? : Option (List MVarId))
+: M m (List Sorry) :=
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let s ← sorries infoTree?.toList prevEnv rootGoals?
+    let restSorries ← sorriesCmd rest state.commandState.env rootGoals?
+    return s ++ restSorries
+
 def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
     Lean.PrettyPrinter.ppTactic ⟨stx⟩
@@ -130,6 +179,46 @@ def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tact
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Tactic.of goals tactic pos endPos proofStateId ns
 
+def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : M m (List Tactic) := do
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let ts ← tactics infoTree?.toList prevEnv
+    let restTactics ← tacticsCmd rest state.commandState.env
+    return ts ++ restTactics
+
+def declTypes (trees: List InfoTree) : M m (List DeclType) := do
+  let exprType: Expr → MetaM String := fun (expr: Expr) => do pure (← Meta.ppExpr (← Lean.Meta.inferType expr)).pretty'
+  let conclusion: Expr → MetaM String := fun (expr: Expr) => do pure (← Meta.ppExpr (← Lean.Meta.forallMetaTelescope (← Meta.inferType expr)).snd.snd).pretty'
+  let treeDecl := (fun t => do
+    let dt := InfoTree.declType t
+    match dt with
+    | some ⟨ctx, expr, stx, lctx, pos, endPos⟩ =>
+      let type := (← ctx.runMetaM lctx (exprType expr))
+      let pp := Format.pretty stx.prettyPrint
+      let conclusionStr ← ctx.runMetaM lctx <| conclusion expr
+      pure [DeclType.of type pp conclusionStr pos endPos]
+    | _ => pure [])
+  trees.flatMapM treeDecl
+
+def namespaces (trees: List InfoTree) : M m (List Namespace) :=
+  trees.flatMap InfoTree.namespaces |>.mapM
+    fun ⟨i, ctx, pos, endPos⟩ =>
+      let openDecls: List String := ctx.openDecls.map toString
+      let pp := (Format.pretty i.stx.prettyPrint)
+      let currNamespace := toString ctx.currNamespace
+      pure (Namespace.of currNamespace pp openDecls pos endPos)
+
+def conclusions (trees: List InfoTree) : M m (List Conclusion) := do
+  let treeDecl := (fun t => do
+    let conc ← InfoTree.conclusion t
+    conc.flatMapM <| fun ⟨info, ctx⟩ => do
+      let pp := Format.pretty info.stx.prettyPrint
+      let range := stxRange ctx.fileMap info.stx
+      pure [Conclusion.of pp range.fst range.snd])
+  trees.flatMapM treeDecl
+
+
 def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
   trees.flatMap InfoTree.rootGoals |>.mapM
     fun ⟨ctx, goals, pos⟩ => do
@@ -138,6 +227,14 @@ def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Sorry.of goals pos pos proofStateId
 
+def collectRootGoalsAsSorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) :
+    M m (List Sorry) := do
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let sorries ← collectRootGoalsAsSorries infoTree?.toList prevEnv
+    let restSorries ← collectRootGoalsAsSorriesCmd rest state.commandState.env
+    return sorries ++ restSorries
 
 private def collectFVarsAux : Expr → NameSet
   | .fvar fvarId => NameSet.empty.insert fvarId.name
@@ -185,6 +282,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
       let res := proofState.runMetaM do
         match proofState.rootGoals with
         | [goalId] =>
+          goalId.withContext do
           match proofState.metaState.mctx.getExprAssignmentCore? goalId with
           | none => return "Error: Goal not assigned"
           | some pf => do
@@ -196,7 +294,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
             unless (← Meta.isDefEq pft expectedType) do
               return s!"Error: proof has type {pft} but root goal has type {expectedType}"
 
-            let pf ← goalId.withContext $ abstractAllLambdaFVars pf
+            let pf ← abstractAllLambdaFVars pf >>= instantiateMVars
             let pft ← Meta.inferType pf >>= instantiateMVars
 
             if pf.hasExprMVar then
@@ -301,19 +399,28 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   if notFound then
     return .inr ⟨"Unknown environment."⟩
   let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
-  let (initialCmdState, cmdState, messages, trees) ← try
-    IO.processInput s.cmd initialCmdState?
+
+  -- Find the best incremental state to reuse based on prefix matching
+  let bestIncrementalState? ← findBestIncrementalState s.cmd s.env
+
+  let (initialCmdState, incStates, messages, headerCache) ← try
+    IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache
   catch ex =>
     return .inr ⟨ex.toString⟩
+
+  modify fun st => { st with headerCache := headerCache }
+
+  -- Store the command text and incremental states for future reuse
+  recordCommandIncrementals s.cmd incStates s.env
+
+  let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState
   let messages ← messages.mapM fun m => Message.of m
-  -- For debugging purposes, sometimes we print out the trees here:
-  -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees initialCmdState.env none
+  let sorries ← sorriesCmd incStates initialCmdState.env none
   let sorries ← match s.rootGoals with
-  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env))
+  | some true => pure (sorries ++ (← collectRootGoalsAsSorriesCmd incStates initialCmdState.env))
   | _ => pure sorries
   let tactics ← match s.allTactics with
-  | some true => tactics trees initialCmdState.env
+  | some true => tacticsCmd incStates initialCmdState.env
   | _ => pure []
   let cmdSnapshot :=
   { cmdState
@@ -323,6 +430,21 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
         snap? := none,
         cancelTk? := none } }
   let env ← recordCommandSnapshot cmdSnapshot
+  let trees := cmdState.infoState.trees.toList
+
+  let decls ← match s.declTypes with
+  | some true => declTypes trees
+  | _ => pure []
+  let namespaces ← match s.namespaces with
+  | some true => namespaces trees
+  | _ => pure []
+  let conclusions ← match s.conclusions with
+  | true => conclusions trees
+  | _ => pure []
+  -- conclusions.forM fun t => do IO.println t.pp
+
+  -- For debugging purposes, sometimes we print out the trees here:
+  -- trees.forM fun t => do IO.println (← t.format)
   let jsonTrees := match s.infotree with
   | some "full" => trees
   | some "tactics" => trees.flatMap InfoTree.retainTacticInfo
@@ -337,7 +459,10 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
     { env,
       messages,
       sorries,
-      tactics
+      tactics,
+      decls,
+      namespaces,
+      conclusions,
       infotree }
 
 def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do
diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index f6936245..d87981e6 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -185,33 +185,44 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot :=
 /-- Pretty print the current goals in the `ProofSnapshot`. -/
 def ppGoals (p : ProofSnapshot) : IO (List Format) :=
   Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·)
+
 /--
 Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals.
-
 For convenience, we also allow a list of `Expr`s, and these are appended to the goals
 as fresh metavariables with the given types.
 -/
-def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
+def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option Environment)
     (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := [])
     : IO ProofSnapshot := do
-  ctx.runMetaM (lctx?.getD {}) do
-    let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
-    let s ← getThe Core.State
-    let s := match env? with
-    | none => s
-    | some env => { s with env }
-    pure <|
-    { coreState := s
-      coreContext := ← readThe Core.Context
-      metaState := ← getThe Meta.State
-      metaContext := ← readThe Meta.Context
-      termState := {}
-      termContext := {}
-      tacticState := { goals }
-      tacticContext := { elaborator := .anonymous }
-      rootGoals := match rootGoals? with
-        | none => goals
-        | some gs => gs }
+  -- Get the local context from the goals if not provided.
+  let lctx ← match lctx? with
+  | none => match goals with
+    | g :: _ => ctx.runMetaM {} do pure (← g.getDecl).lctx
+    | [] => match rootGoals? with
+      | some (g :: _) => ctx.runMetaM {} do pure (← g.getDecl).lctx
+      | _ => pure {}
+  | some lctx => pure lctx
+
+  ctx.runMetaM lctx do
+    -- update local instances, which is necessary when `types` is non-empty
+    Meta.withLocalInstances (lctx.decls.toList.filterMap id) do
+      let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
+      let s ← getThe Core.State
+      let s := match prevEnv? with
+      | none => s
+      | some env => { s with env }
+      pure <|
+      { coreState := s
+        coreContext := ← readThe Core.Context
+        metaState := ← getThe Meta.State
+        metaContext := ← readThe Meta.Context
+        termState := {}
+        termContext := {}
+        tacticState := { goals }
+        tacticContext := { elaborator := .anonymous }
+        rootGoals := match rootGoals? with
+          | none => goals
+          | some gs => gs }
 
 open Lean.Core in
 /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/
diff --git a/test/Mathlib/test/decltypenamespace.expected.out b/test/Mathlib/test/decltypenamespace.expected.out
new file mode 100644
index 00000000..5b9a352e
--- /dev/null
+++ b/test/Mathlib/test/decltypenamespace.expected.out
@@ -0,0 +1,14 @@
+{"env": 0}
+
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 75},
+   "data": "Goals accomplished!"}],
+ "env": 1,
+ "decls":
+ [{"type": "∑ k ∈ Nat.properDivisors 198, k = 270",
+   "pp": "with_namespace",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 22}}]}
+
diff --git a/test/Mathlib/test/decltypenamespace.in b/test/Mathlib/test/decltypenamespace.in
new file mode 100644
index 00000000..da3aef58
--- /dev/null
+++ b/test/Mathlib/test/decltypenamespace.in
@@ -0,0 +1,3 @@
+{"cmd": "import Mathlib.NumberTheory.Divisors"}
+
+{"cmd": "theorem with_namespace  : (∑ k ∈ Nat.properDivisors 198, k) = 270 := by rfl", "env": 0, "declTypes": true}
diff --git a/test/Mathlib/test/decltypeopen.expected.out b/test/Mathlib/test/decltypeopen.expected.out
new file mode 100644
index 00000000..3c555459
--- /dev/null
+++ b/test/Mathlib/test/decltypeopen.expected.out
@@ -0,0 +1,14 @@
+{"env": 0}
+
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 75},
+   "data": "Goals accomplished!"}],
+ "env": 1,
+ "decls":
+ [{"type": "∑ k ∈ properDivisors 198, k = 270",
+   "pp": "with_namespace",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 22}}]}
+
diff --git a/test/Mathlib/test/decltypeopen.in b/test/Mathlib/test/decltypeopen.in
new file mode 100644
index 00000000..9bf153fc
--- /dev/null
+++ b/test/Mathlib/test/decltypeopen.in
@@ -0,0 +1,3 @@
+{"cmd": "import Mathlib.NumberTheory.Divisors\nopen Nat"}
+
+{"cmd": "theorem with_namespace  : (∑ k ∈ Nat.properDivisors 198, k) = 270 := by rfl", "env": 0, "declTypes": true}
diff --git a/test/Mathlib/test/incrementality.expected.out b/test/Mathlib/test/incrementality.expected.out
new file mode 100644
index 00000000..28cbaee6
--- /dev/null
+++ b/test/Mathlib/test/incrementality.expected.out
@@ -0,0 +1,68 @@
+{"tactics":
+ [{"usedConstants":
+   ["Nat.gcd",
+    "HMul.hMul",
+    "Mathlib.Meta.NormNum.isNat_eq_true",
+    "instMulNat",
+    "instOfNatNat",
+    "Mathlib.Meta.NormNum.isNat_ofNat",
+    "Tactic.NormNum.nat_gcd_helper_2",
+    "Nat.instAddMonoidWithOne",
+    "Nat",
+    "Eq.refl",
+    "Mathlib.Meta.NormNum.instAddMonoidWithOneNat",
+    "Tactic.NormNum.isNat_gcd",
+    "OfNat.ofNat",
+    "instHMul"],
+   "tactic": "norm_num",
+   "proofState": 0,
+   "pos": {"line": 2, "column": 60},
+   "goals": "⊢ Nat.gcd 180 168 = 12",
+   "endPos": {"line": 2, "column": 68}},
+  {"usedConstants": ["Eq.refl"],
+   "tactic": "rfl",
+   "proofState": 1,
+   "pos": {"line": 10, "column": 2},
+   "goals": "α✝ : Sort u_1\nn : α✝\n⊢ n = n",
+   "endPos": {"line": 10, "column": 5}}],
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 8, "column": 0},
+   "endPos": {"line": 8, "column": 5},
+   "data": "9227465"}],
+ "env": 0}
+
+{"tactics":
+ [{"usedConstants":
+   ["Nat.gcd",
+    "HMul.hMul",
+    "Mathlib.Meta.NormNum.isNat_eq_true",
+    "instMulNat",
+    "instOfNatNat",
+    "Mathlib.Meta.NormNum.isNat_ofNat",
+    "Tactic.NormNum.nat_gcd_helper_2",
+    "Nat.instAddMonoidWithOne",
+    "Nat",
+    "Eq.refl",
+    "Mathlib.Meta.NormNum.instAddMonoidWithOneNat",
+    "Tactic.NormNum.isNat_gcd",
+    "OfNat.ofNat",
+    "instHMul"],
+   "tactic": "norm_num",
+   "proofState": 2,
+   "pos": {"line": 2, "column": 60},
+   "goals": "⊢ Nat.gcd 180 168 = 12",
+   "endPos": {"line": 2, "column": 68}},
+  {"usedConstants": ["Nat", "Eq.refl"],
+   "tactic": "rfl",
+   "proofState": 3,
+   "pos": {"line": 10, "column": 2},
+   "goals": "n : ℕ\n⊢ n = n + 0",
+   "endPos": {"line": 10, "column": 5}}],
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 8, "column": 0},
+   "endPos": {"line": 8, "column": 5},
+   "data": "9227465"}],
+ "env": 1}
+
diff --git a/test/Mathlib/test/incrementality.in b/test/Mathlib/test/incrementality.in
new file mode 100644
index 00000000..43e5fb5e
--- /dev/null
+++ b/test/Mathlib/test/incrementality.in
@@ -0,0 +1,3 @@
+{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n  | 0 => 0\n  | 1 => 1\n  | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n  rfl", "allTactics": true}
+
+{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n  | 0 => 0\n  | 1 => 1\n  | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n  rfl", "allTactics": true}
diff --git a/test/all_tactics-20250622.expected.out b/test/all_tactics-20250622.expected.out
new file mode 100644
index 00000000..3b16cd5b
--- /dev/null
+++ b/test/all_tactics-20250622.expected.out
@@ -0,0 +1,11 @@
+{"tactics":
+ [{"usedConstants": [],
+   "tactic": "exact hp",
+   "proofState": 0,
+   "pos": {"line": 2, "column": 2},
+   "goals": "P : Prop\nhp : P\n⊢ P",
+   "endPos": {"line": 2, "column": 10}}],
+ "env": 0}
+
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
+
diff --git a/test/all_tactics-20250622.in b/test/all_tactics-20250622.in
new file mode 100644
index 00000000..eeb5153e
--- /dev/null
+++ b/test/all_tactics-20250622.in
@@ -0,0 +1,4 @@
+{"cmd": "example (P : Prop) (hp : P) : P := by\n  exact hp\n", "allTactics": true}
+
+{"tactic": "exact hp", "proofState": 0}
+
diff --git a/test/conclusion.expected.out b/test/conclusion.expected.out
new file mode 100644
index 00000000..d058ad33
--- /dev/null
+++ b/test/conclusion.expected.out
@@ -0,0 +1,33 @@
+{"env": 0,
+ "conclusions":
+ [{"pp": "1 + 1 = 2",
+   "pos": {"line": 1, "column": 12},
+   "endPos": {"line": 1, "column": 21}}]}
+
+{"env": 1}
+
+{"env": 2,
+ "conclusions":
+ [{"pp": "Or a b",
+   "pos": {"line": 2, "column": 32},
+   "endPos": {"line": 2, "column": 38}}]}
+
+{"env": 3}
+
+{"messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 30},
+   "endPos": {"line": 1, "column": 32},
+   "data":
+   "unused variable `ha`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"},
+  {"severity": "warning",
+   "pos": {"line": 1, "column": 39},
+   "endPos": {"line": 1, "column": 41},
+   "data":
+   "unused variable `hb`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}],
+ "env": 4,
+ "conclusions":
+ [{"pp": "∃ (c : Nat), c = 2",
+   "pos": {"line": 1, "column": 49},
+   "endPos": {"line": 1, "column": 67}}]}
+
diff --git a/test/conclusion.in b/test/conclusion.in
new file mode 100644
index 00000000..af77dd63
--- /dev/null
+++ b/test/conclusion.in
@@ -0,0 +1,9 @@
+{"cmd": "theorem f : 1 + 1 = 2 := rfl", "conclusions": true}
+
+{"cmd": "example (P : Prop) (hp : P) : P := by\n  exact hp\n", "conclusions": true}
+
+{"cmd": "variable (a : Prop)\ntheorem f (b : Prop) (hb : b) : Or a b := by\nright\nexact hb", "conclusions": true}
+
+{"cmd": "def f := 37", "conclusions": true}
+
+{"cmd": "theorem a_and_b (a b : Prop) (ha : a) (hb : b) : ∃ (c : Nat), c = 2 := by simp", "conclusions": true}
diff --git a/test/gettype.expected.out b/test/gettype.expected.out
new file mode 100644
index 00000000..359a33c1
--- /dev/null
+++ b/test/gettype.expected.out
@@ -0,0 +1,42 @@
+{"env": 0,
+ "decls":
+ [{"type": "∀ (p : Prop), p → p",
+   "pp": "show_p",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 14}}]}
+
+{"env": 1,
+ "decls":
+ [{"type": "∀ (p : Prop), p → p",
+   "pp": "show_q",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 10}}]}
+
+{"env": 2,
+ "decls":
+ [{"type": "∀ (p : Prop), p → p",
+   "pp": "show_p",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 10}},
+  {"type": "∀ (q : Prop), q → q",
+   "pp": "show_q",
+   "pos": {"line": 3, "column": 4},
+   "endPos": {"line": 3, "column": 10}}]}
+
+{"messages":
+ [{"severity": "warning",
+   "pos": {"line": 2, "column": 12},
+   "endPos": {"line": 2, "column": 13},
+   "data":
+   "unused variable `p`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}],
+ "env": 3,
+ "decls":
+ [{"type": "Prop",
+   "pp": "q",
+   "pos": {"line": 1, "column": 10},
+   "endPos": {"line": 1, "column": 11}},
+  {"type": "∀ (q : Prop) (p : Type), q → q",
+   "pp": "show_q",
+   "pos": {"line": 2, "column": 4},
+   "endPos": {"line": 2, "column": 10}}]}
+
diff --git a/test/gettype.in b/test/gettype.in
new file mode 100644
index 00000000..8d274dcb
--- /dev/null
+++ b/test/gettype.in
@@ -0,0 +1,7 @@
+{"cmd": "theorem show_p (p : Prop) (h : p) : p := by exact h", "declTypes": true}
+
+{"cmd": "def show_q (p : Prop) (h : p) : p := h", "declTypes": true}
+
+{"cmd": "def show_p (p : Prop) (h : p) : p := h\n\ndef show_q (q : Prop) (h : q) : q := h", "declTypes": true}
+
+{"cmd": "variable (q : Prop)\ndef show_q (p : Type) (h : q) : q := h", "declTypes": true}
diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out
new file mode 100644
index 00000000..e3ba5583
--- /dev/null
+++ b/test/in_command_dependency.expected.out
@@ -0,0 +1,45 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 21},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 26}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"},
+  {"severity": "info",
+   "pos": {"line": 2, "column": 22},
+   "endPos": {"line": 2, "column": 28},
+   "data": "Try this: exact x"}],
+ "env": 0}
+
+{"sorries":
+ [{"proofState": 1,
+   "pos": {"line": 1, "column": 21},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 26}},
+  {"proofState": 2,
+   "pos": {"line": 2, "column": 19},
+   "goal": "⊢ False",
+   "endPos": {"line": 2, "column": 24}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"},
+  {"severity": "warning",
+   "pos": {"line": 2, "column": 0},
+   "endPos": {"line": 2, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofStatus": "Completed",
+ "proofState": 3,
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "Try this: exact x"}],
+ "goals": []}
+
diff --git a/test/in_command_dependency.in b/test/in_command_dependency.in
new file mode 100644
index 00000000..78c0b6a9
--- /dev/null
+++ b/test/in_command_dependency.in
@@ -0,0 +1,6 @@
+{"cmd": "theorem x : False := sorry\nexample : False := by exact?"}
+
+{"cmd": "theorem x : False := sorry\nexample : False := sorry"}
+
+{"proofState": 2, "tactic": "exact?"}
+
diff --git a/test/local_instance_proof.expected.out b/test/local_instance_proof.expected.out
new file mode 100644
index 00000000..5a93d082
--- /dev/null
+++ b/test/local_instance_proof.expected.out
@@ -0,0 +1,62 @@
+{"env": 0}
+
+{"env": 1}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 42},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 47}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 2}
+
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
+
+{"sorries":
+ [{"proofState": 2,
+   "pos": {"line": 1, "column": 45},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 50}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 3}
+
+{"proofStatus": "Completed", "proofState": 3, "goals": []}
+
+{"env": 4}
+
+{"sorries":
+ [{"proofState": 4,
+   "pos": {"line": 1, "column": 17},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 22}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 5}
+
+{"proofStatus": "Completed", "proofState": 5, "goals": []}
+
+{"sorries":
+ [{"proofState": 6,
+   "pos": {"line": 1, "column": 20},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 25}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 6}
+
+{"proofStatus": "Completed", "proofState": 7, "goals": []}
+
diff --git a/test/local_instance_proof.in b/test/local_instance_proof.in
new file mode 100644
index 00000000..eeefd5ef
--- /dev/null
+++ b/test/local_instance_proof.in
@@ -0,0 +1,21 @@
+{"cmd": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s"}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := test α", "env": 0}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := sorry", "env": 0}
+
+{"tactic": "exact test α", "proofState": 0}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := by sorry", "env": 0}
+
+{"tactic": "exact test α", "proofState": 2}
+
+{"cmd": "variable (α : Type) [s : Inhabited α]", "env": 0}
+
+{"cmd": "def test2 : α := sorry", "env": 4}
+
+{"tactic": "exact test α", "proofState": 4}
+
+{"cmd": "def test2 : α := by sorry", "env": 4}
+
+{"tactic": "exact test α", "proofState": 6}
diff --git a/test/namespaces.expected.out b/test/namespaces.expected.out
new file mode 100644
index 00000000..00ac54f9
--- /dev/null
+++ b/test/namespaces.expected.out
@@ -0,0 +1,41 @@
+{"namespaces":
+ [{"pp": "namespace Lean",
+   "pos": {"line": 1, "column": 0},
+   "openDecls": [],
+   "endPos": {"line": 1, "column": 14},
+   "currentNamespace": "Lean"},
+  {"pp": "open Nat",
+   "pos": {"line": 2, "column": 0},
+   "openDecls": ["Nat"],
+   "endPos": {"line": 2, "column": 8},
+   "currentNamespace": "Lean"},
+  {"pp": "open Elab",
+   "pos": {"line": 3, "column": 0},
+   "openDecls": ["Lean.Elab", "Nat"],
+   "endPos": {"line": 3, "column": 9},
+   "currentNamespace": "Lean"}],
+ "env": 0}
+
+{"namespaces":
+ [{"pp": "open Lean",
+   "pos": {"line": 1, "column": 0},
+   "openDecls": ["Lean", "Lean.Elab", "Nat"],
+   "endPos": {"line": 1, "column": 9},
+   "currentNamespace": "Lean"},
+  {"pp": "section test",
+   "pos": {"line": 2, "column": 0},
+   "openDecls": ["Lean", "Lean.Elab", "Nat"],
+   "endPos": {"line": 2, "column": 12},
+   "currentNamespace": "Lean"},
+  {"pp": "open Nat",
+   "pos": {"line": 3, "column": 0},
+   "openDecls": ["Nat", "Lean", "Lean.Elab", "Nat"],
+   "endPos": {"line": 3, "column": 8},
+   "currentNamespace": "Lean"},
+  {"pp": "end test",
+   "pos": {"line": 4, "column": 0},
+   "openDecls": ["Lean", "Lean.Elab", "Nat"],
+   "endPos": {"line": 4, "column": 8},
+   "currentNamespace": "Lean"}],
+ "env": 1}
+
diff --git a/test/namespaces.in b/test/namespaces.in
new file mode 100644
index 00000000..c2ef97ea
--- /dev/null
+++ b/test/namespaces.in
@@ -0,0 +1,3 @@
+{"cmd": "namespace Lean\nopen Nat\nopen Elab", "namespaces": true}
+
+{"cmd": "open Lean\nsection test\nopen Nat\nend test", "namespaces": true, "env": 0}
diff --git a/test/sections.expected.out b/test/sections.expected.out
new file mode 100644
index 00000000..5ff601e3
--- /dev/null
+++ b/test/sections.expected.out
@@ -0,0 +1,79 @@
+{"namespaces":
+ [{"pp": "section",
+   "pos": {"line": 1, "column": 0},
+   "openDecls": [],
+   "endPos": {"line": 1, "column": 7},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "open Nat",
+   "pos": {"line": 2, "column": 0},
+   "openDecls": ["Nat"],
+   "endPos": {"line": 2, "column": 8},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "end",
+   "pos": {"line": 3, "column": 0},
+   "openDecls": [],
+   "endPos": {"line": 3, "column": 3},
+   "currentNamespace": "[anonymous]"}],
+ "env": 0}
+
+{"namespaces":
+ [{"pp": "open Lean",
+   "pos": {"line": 1, "column": 0},
+   "openDecls": ["Lean"],
+   "endPos": {"line": 1, "column": 9},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "section test",
+   "pos": {"line": 2, "column": 0},
+   "openDecls": ["Lean"],
+   "endPos": {"line": 2, "column": 12},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "open Nat",
+   "pos": {"line": 3, "column": 0},
+   "openDecls": ["Nat", "Lean"],
+   "endPos": {"line": 3, "column": 8},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "end test",
+   "pos": {"line": 4, "column": 0},
+   "openDecls": ["Lean"],
+   "endPos": {"line": 4, "column": 8},
+   "currentNamespace": "[anonymous]"}],
+ "env": 1}
+
+{"namespaces":
+ [{"pp": "open Lean",
+   "pos": {"line": 1, "column": 0},
+   "openDecls": ["Lean"],
+   "endPos": {"line": 1, "column": 9},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "section",
+   "pos": {"line": 2, "column": 0},
+   "openDecls": ["Lean"],
+   "endPos": {"line": 2, "column": 7},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "open Nat",
+   "pos": {"line": 3, "column": 0},
+   "openDecls": ["Nat", "Lean"],
+   "endPos": {"line": 3, "column": 8},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "section test",
+   "pos": {"line": 4, "column": 0},
+   "openDecls": ["Nat", "Lean"],
+   "endPos": {"line": 4, "column": 12},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "open Elab",
+   "pos": {"line": 5, "column": 0},
+   "openDecls": ["Lean.Elab", "Nat", "Lean"],
+   "endPos": {"line": 5, "column": 9},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "end test",
+   "pos": {"line": 6, "column": 0},
+   "openDecls": ["Nat", "Lean"],
+   "endPos": {"line": 6, "column": 8},
+   "currentNamespace": "[anonymous]"},
+  {"pp": "end",
+   "pos": {"line": 7, "column": 0},
+   "openDecls": ["Lean"],
+   "endPos": {"line": 7, "column": 3},
+   "currentNamespace": "[anonymous]"}],
+ "env": 2}
+
diff --git a/test/sections.in b/test/sections.in
new file mode 100644
index 00000000..ab64af73
--- /dev/null
+++ b/test/sections.in
@@ -0,0 +1,5 @@
+{"cmd": "section\nopen Nat\nend", "namespaces": true}
+
+{"cmd": "open Lean\nsection test\nopen Nat\nend test", "namespaces": true}
+
+{"cmd": "open Lean\nsection\nopen Nat\nsection test\nopen Elab\nend test\nend", "namespaces": true}