feat: add addContext

src/Init/Lean/Elab/Command.lean

@@ -74,10 +74,19 @@ instance CommandElabCoreM.monadState : MonadState State CommandElabM :=
   set       := setState,
   modifyGet := @modifyGetState }
 
+def getEnv : CommandElabM Environment := do s ← get; pure s.env
+def getScope : CommandElabM Scope := do s ← get; pure s.scopes.head!
+def getOptions : CommandElabM Options := do scope ← getScope; pure scope.opts
+
+def addContext (msg : MessageData) : CommandElabM MessageData := do
+env ← getEnv; opts ← getOptions;
+pure (MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msg)
+
 instance CommandElabM.monadLog : MonadLog CommandElabM :=
 { getCmdPos   := do ctx ← read; pure ctx.cmdPos,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
+  addContext  := addContext,
   logMessage  := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
 
 /- If `ref` does not have position information, then try to use macroStack -/
@@ -243,18 +252,9 @@ fun ctx => EIO.catchExceptions (withLogging x ctx) (fun _ => pure ())
 def dbgTrace {α} [HasToString α] (a : α) : CommandElabM Unit :=
 _root_.dbgTrace (toString a) $ fun _ => pure ()
 
-def getEnv : CommandElabM Environment := do
-s ← get; pure s.env
-
 def setEnv (newEnv : Environment) : CommandElabM Unit :=
 modify $ fun s => { env := newEnv, .. s }
 
-def getScope : CommandElabM Scope := do
-s ← get; pure s.scopes.head!
-
-def getOptions : CommandElabM Options := do
-scope ← getScope; pure scope.opts
-
 def getCurrNamespace : CommandElabM Name := do
 scope ← getScope; pure scope.currNamespace
 

src/Init/Lean/Elab/Level.lean

@@ -27,7 +27,8 @@ abbrev LevelElabM := ReaderT Context (EStateM Exception State)
 instance LevelElabM.MonadLog : MonadPosInfo LevelElabM :=
 { getCmdPos   := do ctx ← read; pure ctx.cmdPos,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
-  getFileName := do ctx ← read; pure ctx.fileName }
+  getFileName := do ctx ← read; pure ctx.fileName,
+  addContext  := fun msg => pure msg }
 
 def mkFreshId : LevelElabM Name := do
 s ← get;

src/Init/Lean/Elab/Log.lean

@@ -14,6 +14,7 @@ class MonadPosInfo (m : Type → Type) :=
 (getFileMap  {} : m FileMap)
 (getFileName {} : m String)
 (getCmdPos   {} : m String.Pos)
+(addContext  {} : MessageData → m MessageData)
 
 export MonadPosInfo (getFileMap getFileName getCmdPos)
 
@@ -34,6 +35,7 @@ fileMap ← getFileMap;
 fileName ← getFileName;
 cmdPos ← getCmdPos;
 let pos := fileMap.toPosition (pos.getD cmdPos);
+msgData ← MonadPosInfo.addContext msgData;
 pure { fileName := fileName, pos := pos, data := msgData, severity := severity }
 
 def getPos [MonadPosInfo m] (stx : Syntax) : m String.Pos :=

src/Init/Lean/Elab/Term.lean

@@ -101,10 +101,21 @@ match result with
 | EStateM.Result.ok e s     => do set s; pure e
 | EStateM.Result.error ex s => do set s; throw (Exception.error ex)
 
+def getEnv : TermElabM Environment := do s ← get; pure s.env
+def getMCtx : TermElabM MetavarContext := do s ← get; pure s.mctx
+def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx
+def getLocalInsts : TermElabM LocalInstances := do ctx ← read; pure ctx.localInstances
+def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts
+
+def addContext (msg : MessageData) : TermElabM MessageData := do
+env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
+pure (MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msg)
+
 instance TermElabM.MonadLog : MonadLog TermElabM :=
 { getCmdPos   := do ctx ← read; pure ctx.cmdPos,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
+  addContext  := addContext,
   logMessage  := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
 
 /- If `ref` does not have position information, then try to use macroStack -/
@@ -216,14 +227,9 @@ inductive LVal
 instance LVal.hasToString : HasToString LVal :=
 ⟨fun p => match p with | LVal.fieldIdx i => toString i | LVal.fieldName n => n | LVal.getOp idx => "[" ++ toString idx ++ "]"⟩
 
-def getEnv : TermElabM Environment := do s ← get; pure s.env
-def getMCtx : TermElabM MetavarContext := do s ← get; pure s.mctx
 def getDeclName? : TermElabM (Option Name) := do ctx ← read; pure ctx.declName?
 def getCurrNamespace : TermElabM Name := do ctx ← read; pure ctx.currNamespace
 def getOpenDecls : TermElabM (List OpenDecl) := do ctx ← read; pure ctx.openDecls
-def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx
-def getLocalInsts : TermElabM LocalInstances := do ctx ← read; pure ctx.localInstances
-def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts
 def getTraceState : TermElabM TraceState := do s ← get; pure s.traceState
 def setTraceState (traceState : TraceState) : TermElabM Unit := modify $ fun s => { traceState := traceState, .. s }
 def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := do mctx ← getMCtx; pure $ mctx.isExprAssigned mvarId