diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 411eec30f6..f5ed37d175 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -285,7 +285,7 @@ fType ← instantiateMVars fType;
 trace `Elab.app.args $ fun _ => "explicit: " ++ toString explicit ++ ", " ++ f ++ " : " ++ fType;
 unless (namedArgs.isEmpty && args.isEmpty) $
   tryPostponeIfMVar fType;
-ref ← getCurrRef;
+ref ← getRef;
 elabAppArgsAux {ref := ref, args := args, expectedType? := expectedType?, explicit := explicit, namedArgs := namedArgs } f fType
 
 /-- Auxiliary inductive datatype that represents the resolution of an `LVal`. -/
@@ -554,20 +554,19 @@ candidates.filter $ fun c => match c with
   | EStateM.Result.ok _ _ => true
   | _ => false
 
-private def toMessageData (msg : Message) (stx : Syntax) : TermElabM MessageData := do
-strPos ← getPos stx;
-pos ← getPosition strPos;
+private def toMessageData (msg : Message) : TermElabM MessageData := do
+pos ← getRefPosition;
 if pos == msg.pos then
   pure msg.data
 else
   pure $ toString msg.pos.line ++ ":" ++ toString msg.pos.column ++ " " ++ msg.data
 
-private def mergeFailures {α} (failures : Array TermElabResult) (stx : Syntax) : TermElabM α := do
+private def mergeFailures {α} (failures : Array TermElabResult) : TermElabM α := do
 msgs ← failures.mapM $ fun failure =>
   match failure with
   | EStateM.Result.ok _ _         => unreachable!
-  | EStateM.Result.error errMsg s => toMessageData errMsg stx;
-throwErrorAt stx ("overloaded, errors " ++ MessageData.ofArray msgs)
+  | EStateM.Result.error errMsg s => toMessageData errMsg;
+throwError ("overloaded, errors " ++ MessageData.ofArray msgs)
 
 private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) : TermElabM Expr := do
 /- TODO: if `f` contains `choice` or overloaded symbols, `mayPostpone == true`, and `expectedType? == some ?m` where `?m` is not assigned,
@@ -590,7 +589,7 @@ else
       | _                     => unreachable!;
     throwErrorAt f ("ambiguous, possible interpretations " ++ MessageData.ofArray msgs)
   else
-    mergeFailures candidates f
+    withRef f $ mergeFailures candidates
 
 private partial def expandApp (stx : Syntax) : TermElabM (Syntax × Array NamedArg × Array Arg) := do
 let f    := stx.getArg 0;
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index eff251ed8c..c5565b3ed0 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -46,6 +46,7 @@ structure Context :=
 (cmdPos         : String.Pos := 0)
 (macroStack     : MacroStack := [])
 (currMacroScope : MacroScope := firstFrontendMacroScope)
+(ref            : Syntax := Syntax.missing)
 
 instance Exception.inhabited : Inhabited Exception := ⟨Exception.error $ arbitrary _⟩
 
@@ -53,6 +54,14 @@ abbrev CommandElabCoreM (ε) := ReaderT Context (EIO ε)
 abbrev CommandElabM := CommandElabCoreM Exception
 abbrev CommandElab  := Syntax → CommandElabM Unit
 
+@[inline] def getCurrRef : CommandElabM Syntax := do
+ctx ← read;
+pure ctx.ref
+
+/- Execute `x` using using `ref` as the default Syntax for providing position information to error messages. -/
+@[inline] def withRef {α} (ref : Syntax) (x : CommandElabM α) : CommandElabM α := do
+adaptReader (fun (ctx : Context) => { ctx with ref := replaceRef ref ctx.ref }) x
+
 def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
 mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
 
@@ -63,14 +72,14 @@ mkMessageAux ctx ref (addMacroStack (toString err) ctx.macroStack) MessageSeveri
 @[inline] def liftIOCore {α} (ctx : Context) (ref : Syntax) (x : IO α) : EIO Exception α :=
 EIO.adaptExcept (fun ex => Exception.error $ ioErrorToMessage ctx ref ex) x
 
-@[inline] def liftIO {α} (ref : Syntax) (x : IO α) : CommandElabM α :=
-fun ctx => liftIOCore ctx ref x
+@[inline] def liftIO {α} (x : IO α) : CommandElabM α :=
+fun ctx => liftIOCore ctx ctx.ref x
 
 private def getState : CommandElabM State :=
-fun ctx => liftIOCore ctx Syntax.missing $ ctx.stateRef.get
+fun ctx => liftIOCore ctx ctx.ref $ ctx.stateRef.get
 
 private def setState (s : State) : CommandElabM Unit :=
-fun ctx => liftIOCore ctx Syntax.missing $ ctx.stateRef.set s
+fun ctx => liftIOCore ctx ctx.ref $ ctx.stateRef.set s
 
 @[inline] private def modifyGetState {α} (f : State → α × State) : CommandElabM α := do
 s ← getState; let (a, s) := f s; setState s; pure a
@@ -89,7 +98,7 @@ 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,
+{ getRef      := do ctx ← read; pure ctx.ref,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
   addContext  := addContext,
@@ -98,20 +107,24 @@ instance CommandElabM.monadLog : MonadLog CommandElabM :=
 /--
   Throws an error with the given `msgData` and extracting position information from `ref`.
   If `ref` does not contain position information, then use `cmdPos` -/
-def throwError {α} (ref : Syntax) (msgData : MessageData) : CommandElabM α := do
+def throwError {α} (msgData : MessageData) : CommandElabM α := do
 ctx ← read;
-let ref     := getBetterRef ref ctx.macroStack;
+let ref     := getBetterRef ctx.ref ctx.macroStack;
 let msgData := addMacroStack msgData ctx.macroStack;
-msg ← mkMessage msgData MessageSeverity.error ref;
-throw (Exception.error msg)
+withRef ref do
+  msg ← mkMessage msgData MessageSeverity.error;
+  throw (Exception.error msg)
 
-def logTrace (cls : Name) (ref : Syntax) (msg : MessageData) : CommandElabM Unit := do
+def throwErrorAt {α} (ref : Syntax) (msgData : MessageData) : CommandElabM α :=
+withRef ref $ throwError msgData
+
+def logTrace (cls : Name) (msg : MessageData) : CommandElabM Unit := do
 msg ← addContext $ MessageData.tagged cls msg;
-logInfo ref msg
+logInfo msg
 
-@[inline] def trace (cls : Name) (ref : Syntax) (msg : Unit → MessageData) : CommandElabM Unit := do
+@[inline] def trace (cls : Name) (msg : Unit → MessageData) : CommandElabM Unit := do
 opts ← getOptions;
-when (checkTraceOption opts cls) $ logTrace cls ref (msg ())
+when (checkTraceOption opts cls) $ logTrace cls (msg ())
 
 def throwUnsupportedSyntax {α} : CommandElabM α :=
 throw Elab.Exception.unsupportedSyntax
@@ -133,15 +146,15 @@ unsafe def mkCommandElabAttribute : IO (KeyedDeclsAttribute CommandElab) :=
 mkElabAttribute CommandElab `Lean.Elab.Command.commandElabAttribute `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command"
 @[init mkCommandElabAttribute] constant commandElabAttribute : KeyedDeclsAttribute CommandElab := arbitrary _
 
-@[inline] def withIncRecDepth {α} (ref : Syntax) (x : CommandElabM α) : CommandElabM α := do
+@[inline] def withIncRecDepth {α} (x : CommandElabM α) : CommandElabM α := do
 ctx ← read; s ← get;
-when (ctx.currRecDepth == s.maxRecDepth) $ throwError ref maxRecDepthErrorMessage;
+when (ctx.currRecDepth == s.maxRecDepth) $ throwError maxRecDepthErrorMessage;
 adaptReader (fun (ctx : Context) => { ctx with currRecDepth := ctx.currRecDepth + 1 }) x
 
 private def elabCommandUsing (s : State) (stx : Syntax) : List CommandElab → CommandElabM Unit
 | []                => do
   let refFmt := stx.prettyPrint;
-  throwError stx ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
+  throwError ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
 | (elabFn::elabFns) => catch (elabFn stx)
   (fun ex => match ex with
     | Exception.error _           => throw ex
@@ -158,18 +171,18 @@ instance : MonadMacroAdapter CommandElabM :=
   setNextMacroScope      := fun next => modify $ fun s => { s with nextMacroScope := next },
   getCurrRecDepth        := do ctx ← read; pure ctx.currRecDepth,
   getMaxRecDepth         := do s ← get; pure s.maxRecDepth,
-  throwError             := @throwError,
+  throwError             := @throwErrorAt,
   throwUnsupportedSyntax := @throwUnsupportedSyntax}
 
 partial def elabCommand : Syntax → CommandElabM Unit
-| stx => withIncRecDepth stx $ withFreshMacroScope $ match stx with
+| stx => withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with
   | Syntax.node k args =>
     if k == nullKind then
       -- list of commands => elaborate in order
       -- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
       args.forM elabCommand
     else do
-      trace `Elab.step stx $ fun _ => stx;
+      trace `Elab.step fun _ => stx;
       s ← get;
       stxNew? ← catch
         (do newStx ← adaptMacro (getMacros s.env) stx; pure (some newStx))
@@ -183,8 +196,8 @@ partial def elabCommand : Syntax → CommandElabM Unit
         let k := stx.getKind;
         match table.find? k with
         | some elabFns => elabCommandUsing s stx elabFns
-        | none         => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
-  | _ => throwError stx "unexpected command"
+        | none         => throwError ("elaboration function for '" ++ toString k ++ "' has not been implemented")
+  | _ => throwError "unexpected command"
 
 /-- Adapt a syntax transformation to a regular, command-producing elaborator. -/
 def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab :=
@@ -199,13 +212,13 @@ let scope := s.scopes.head!;
   fileMap        := ctx.fileMap,
   currRecDepth   := ctx.currRecDepth,
   maxRecDepth    := s.maxRecDepth,
-  cmdPos         := ctx.cmdPos,
   declName?      := declName?,
   macroStack     := ctx.macroStack,
   currMacroScope := ctx.currMacroScope,
   currNamespace  := scope.currNamespace,
   levelNames     := scope.levelNames,
-  openDecls      := scope.openDecls }
+  openDecls      := scope.openDecls,
+  ref            := ctx.ref }
 
 private def mkTermState (s : State) : Term.State :=
 { env            := s.env,
@@ -257,25 +270,25 @@ modify $ fun s => {
   scopes := { s.scopes.head! with kind := kind, header := header, currNamespace := newNamespace } :: s.scopes
 }
 
-private def addScopes (ref : Syntax) (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
+private def addScopes (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
 | Name.anonymous => pure ()
 | Name.str p header _ => do
   addScopes p;
   currNamespace ← getCurrNamespace;
   addScope kind header (if updateNamespace then currNamespace ++ header else currNamespace)
-| _ => throwError ref "invalid scope"
+| _ => throwError "invalid scope"
 
-private def addNamespace (ref : Syntax) (header : Name) : CommandElabM Unit :=
-addScopes ref "namespace" true header
+private def addNamespace (header : Name) : CommandElabM Unit :=
+addScopes "namespace" true header
 
 @[builtinCommandElab «namespace»] def elabNamespace : CommandElab :=
 fun stx => match_syntax stx with
-  | `(namespace $n) => addNamespace stx n.getId
+  | `(namespace $n) => addNamespace n.getId
   | _               => throw Exception.unsupportedSyntax
 
 @[builtinCommandElab «section»] def elabSection : CommandElab :=
 fun stx => match_syntax stx with
-  | `(section $header:ident) => addScopes stx "section" false header.getId
+  | `(section $header:ident) => addScopes "section" false header.getId
   | `(section)               => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
   | _                        => throw Exception.unsupportedSyntax
 
@@ -303,14 +316,14 @@ fun stx => do
   else do {
     -- we keep "root" scope
     modify $ fun s => { s with scopes := s.scopes.drop (s.scopes.length - 1) };
-    throwError stx "invalid 'end', insufficient scopes"
+    throwError "invalid 'end', insufficient scopes"
   };
   match header? with
-  | none        => unless (checkAnonymousScope scopes) $ throwError stx "invalid 'end', name is missing"
-  | some header => unless (checkEndHeader header scopes) $ throwError stx "invalid 'end', name mismatch"
+  | none        => unless (checkAnonymousScope scopes) $ throwError "invalid 'end', name is missing"
+  | some header => unless (checkEndHeader header scopes) $ throwError "invalid 'end', name mismatch"
 
-@[inline] def withNamespace {α} (ref : Syntax) (ns : Name) (elabFn : CommandElabM α) : CommandElabM α := do
-addNamespace ref ns;
+@[inline] def withNamespace {α} (ns : Name) (elabFn : CommandElabM α) : CommandElabM α := do
+addNamespace ns;
 a ← elabFn;
 modify $ fun s => { s with scopes := s.scopes.drop ns.getNumParts };
 pure a
@@ -325,14 +338,15 @@ modify $ fun s =>
 def getLevelNames : CommandElabM (List Name) := do
 scope ← getScope; pure scope.levelNames
 
-def throwAlreadyDeclaredUniverseLevel {α} (ref : Syntax) (u : Name) : CommandElabM α :=
-throwError ref ("a universe level named '" ++ toString u ++ "' has already been declared")
+def throwAlreadyDeclaredUniverseLevel {α} (u : Name) : CommandElabM α :=
+throwError ("a universe level named '" ++ toString u ++ "' has already been declared")
 
-def addUnivLevel (idStx : Syntax) : CommandElabM Unit := do
+def addUnivLevel (idStx : Syntax) : CommandElabM Unit :=
+withRef idStx do
 let id := idStx.getId;
 levelNames ← getLevelNames;
 if levelNames.elem id then
-  throwAlreadyDeclaredUniverseLevel idStx id
+  throwAlreadyDeclaredUniverseLevel id
 else
   modifyScope $ fun scope => { scope with levelNames := id :: scope.levelNames }
 
@@ -367,13 +381,13 @@ fun stx => do
   | Except.ok env   => setEnv env
   | Except.error ex => do
     opts ← getOptions;
-    throwError stx (ex.toMessageData opts)
+    throwError (ex.toMessageData opts)
 
 def getOpenDecls : CommandElabM (List OpenDecl) := do
 scope ← getScope; pure scope.openDecls
 
-def logUnknownDecl (stx : Syntax) (declName : Name) : CommandElabM Unit :=
-logError stx ("unknown declaration '" ++ toString declName ++ "'")
+def logUnknownDecl (declName : Name) : CommandElabM Unit :=
+logError ("unknown declaration '" ++ toString declName ++ "'")
 
 def resolveNamespace (id : Name) : CommandElabM Name := do
 env           ← getEnv;
@@ -389,7 +403,7 @@ fun stx => do
   let id  := stx.getIdAt 1;
   ns ← resolveNamespace id;
   currNamespace ← getCurrNamespace;
-  when (ns == currNamespace) $ throwError stx "invalid 'export', self export";
+  when (ns == currNamespace) $ throwError "invalid 'export', self export";
   env ← getEnv;
   let ids := (stx.getArg 3).getArgs;
   aliases ← ids.foldlM
@@ -399,7 +413,7 @@ fun stx => do
       if env.contains declName then
         pure $ (currNamespace ++ id, declName) :: aliases
       else do
-        logUnknownDecl idStx declName;
+        withRef idStx $ logUnknownDecl declName;
         pure aliases
       })
     [];
@@ -427,7 +441,7 @@ ids.forArgsM $ fun idStx => do
   if env.contains declName then
     addOpenDecl (OpenDecl.explicit id declName)
   else
-    logUnknownDecl idStx declName
+    withRef idStx $ logUnknownDecl declName
 
 -- `open` id `hiding` id+
 def elabOpenHiding (n : SyntaxNode) : CommandElabM Unit := do
@@ -441,7 +455,7 @@ ids : List Name ← idsStx.foldArgsM (fun idStx ids => do
   if env.contains declName then
     pure (id::ids)
   else do
-    logUnknownDecl idStx declName;
+    withRef idStx $ logUnknownDecl declName;
     pure ids)
   [];
 addOpenDecl (OpenDecl.simple ns ids)
@@ -459,7 +473,7 @@ rs.forSepArgsM $ fun stx => do
   if env.contains declName then
     addOpenDecl (OpenDecl.explicit toId declName)
   else
-    logUnknownDecl stx declName
+    withRef stx $ logUnknownDecl declName
 
 @[builtinCommandElab «open»] def elabOpen : CommandElab :=
 fun n => do
@@ -501,13 +515,13 @@ fun stx => do
     e    ← Term.elabTerm term none;
     Term.synthesizeSyntheticMVars false;
     type ← Term.inferType e;
-    logInfo stx (e ++ " : " ++ type);
+    logInfo (e ++ " : " ++ type);
     pure ()
 
 def hasNoErrorMessages : CommandElabM Bool := do
 s ← get; pure $ !s.messages.hasErrors
 
-def failIfSucceeds (ref : Syntax) (x : CommandElabM Unit) : CommandElabM Unit := do
+def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
 let resetMessages : CommandElabM MessageLog := do {
   s ← get;
   let messages := s.messages;
@@ -523,20 +537,20 @@ succeeded ← finally
      (do x; hasNoErrorMessages)
      (fun ex => match ex with
        | Exception.error msg         => do modify (fun s => { s with messages := s.messages.add msg }); pure false
-       | Exception.unsupportedSyntax => do logError ref "unsupported syntax"; pure false))
+       | Exception.unsupportedSyntax => do logError "unsupported syntax"; pure false))
   (restoreMessages prevMessages);
 when succeeded $
-  throwError ref "unexpected success"
+  throwError "unexpected success"
 
 @[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab :=
-fun stx => failIfSucceeds stx $ elabCheck stx
+fun stx => failIfSucceeds $ elabCheck stx
 
 def addDecl (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.addDecl decl
 def compileDecl (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.compileDecl decl
 
-def addInstance (ref : Syntax) (declName : Name) : CommandElabM Unit := do
+def addInstance (declName : Name) : CommandElabM Unit := do
 env ← getEnv;
-env ← liftIO ref $ Meta.addGlobalInstance env declName;
+env ← liftIO $ Meta.addGlobalInstance env declName;
 setEnv env
 
 unsafe def elabEvalUnsafe : CommandElab :=
@@ -569,8 +583,8 @@ fun stx => withoutModifyingEnv do
         | Except.error e => Term.throwError e
         | Except.ok act  => pure $ act env opts
     };
-    (out, res) ← liftIO ref $ IO.Prim.withIsolatedStreams act;
-    logInfo ref out;
+    (out, res) ← liftIO $ IO.Prim.withIsolatedStreams act;
+    logInfo out;
     match res with
     | Except.error e => throw $ Exception.error $ ioErrorToMessage ctx ref e
     | Except.ok env  => do setEnv env; pure ()
@@ -588,8 +602,8 @@ fun stx => withoutModifyingEnv do
       | Except.error e => Term.throwError e
       | Except.ok act  => pure act
     };
-    (out, res) ← liftIO ref $ IO.Prim.withIsolatedStreams act;
-    logInfo ref out;
+    (out, res) ← liftIO $ IO.Prim.withIsolatedStreams act;
+    logInfo out;
     match res with
     | Except.error e => throw $ Exception.error $ ioErrorToMessage ctx ref e
     | Except.ok _    => pure ()
@@ -604,19 +618,18 @@ constant elabEval : CommandElab := arbitrary _
 
 @[builtinCommandElab «synth»] def elabSynth : CommandElab :=
 fun stx => do
-  let ref  := stx;
   let term := stx.getArg 1;
   withoutModifyingEnv $ runTermElabM `_synth_cmd $ fun _ => do
     inst ← Term.elabTerm term none;
     Term.synthesizeSyntheticMVars false;
     inst ← Term.instantiateMVars inst;
     val  ← Term.liftMetaM $ Meta.synthInstance inst;
-    logInfo stx val;
+    logInfo val;
     pure ()
 
-def setOption (ref : Syntax) (optionName : Name) (val : DataValue) : CommandElabM Unit := do
-decl ← liftIO ref $ getOptionDecl optionName;
-unless (decl.defValue.sameCtor val) $ throwError ref "type mismatch at set_option";
+def setOption (optionName : Name) (val : DataValue) : CommandElabM Unit := do
+decl ← liftIO $ getOptionDecl optionName;
+unless (decl.defValue.sameCtor val) $ throwError "type mismatch at set_option";
 modifyScope $ fun scope => { scope with opts := scope.opts.insert optionName val };
 match optionName, val with
 | `maxRecDepth, DataValue.ofNat max => modify $ fun s => { s with maxRecDepth := max }
@@ -624,19 +637,18 @@ match optionName, val with
 
 @[builtinCommandElab «set_option»] def elabSetOption : CommandElab :=
 fun stx => do
-  let ref        := stx;
   let optionName := stx.getIdAt 1;
   let val        := stx.getArg 2;
   match val.isStrLit? with
-  | some str => setOption ref optionName (DataValue.ofString str)
+  | some str => setOption optionName (DataValue.ofString str)
   | none     =>
   match val.isNatLit? with
-  | some num => setOption ref optionName (DataValue.ofNat num)
+  | some num => setOption optionName (DataValue.ofNat num)
   | none     =>
   match val with
-  | Syntax.atom _ "true"  => setOption ref optionName (DataValue.ofBool true)
-  | Syntax.atom _ "false" => setOption ref optionName (DataValue.ofBool false)
-  | _ => logError val ("unexpected set_option value " ++ toString val)
+  | Syntax.atom _ "true"  => setOption optionName (DataValue.ofBool true)
+  | Syntax.atom _ "false" => setOption optionName (DataValue.ofBool false)
+  | _ => withRef val $ logError ("unexpected set_option value " ++ toString val)
 
 /-
   `declId` is of the form
@@ -666,12 +678,12 @@ levelNames      ←
       (fun levelNames idStx =>
         let id := idStx.getId;
         if levelNames.elem id then
-          throwAlreadyDeclaredUniverseLevel idStx id
+          withRef idStx $ throwAlreadyDeclaredUniverseLevel id
         else
           pure (id :: levelNames))
       savedLevelNames
   };
-let ref := declId;
+withRef declId $
 -- extract (optional) namespace part of id, after decoding macro scopes that would interfere with the check
 let scpView := extractMacroScopes id;
 match scpView.name with
@@ -679,10 +691,10 @@ match scpView.name with
   /- Add back macro scopes. We assume a declaration like `def a.b[1,2] ...` with macro scopes `[1,2]`
      is always meant to mean `namespace a def b[1,2] ...`. -/
   let id := { scpView with name := mkNameSimple s }.review;
-  withNamespace ref pre $ do
+  withNamespace pre $ do
     modifyScope $ fun scope => { scope with levelNames := levelNames };
     finally (f id) (modifyScope $ fun scope => { scope with levelNames := savedLevelNames })
-| _ => throwError ref "invalid declaration name"
+| _ => throwError "invalid declaration name"
 
 /--
   Sort the given list of `usedParams` using the following order:
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index f0f6fd08f2..a51b0796aa 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -67,11 +67,11 @@ def elabAttr (stx : Syntax) : CommandElabM Attribute := do
 -- rawIdent >> many attrArg
 let nameStx := stx.getArg 0;
 attrName ← match nameStx.isIdOrAtom? with
-  | none     => throwError nameStx "identifier expected"
+  | none     => withRef nameStx $ throwError "identifier expected"
   | some str => pure $ mkNameSimple str;
 env ← getEnv;
 unless (isAttribute env attrName) $
-  throwError stx ("unknown attribute [" ++ attrName ++ "]");
+  throwError ("unknown attribute [" ++ attrName ++ "]");
 let args := stx.getArg 1;
 -- the old frontend passes Syntax.missing for empty args, for reasons
 let args := if args.getNumArgs == 0 then Syntax.missing else args;
@@ -95,14 +95,14 @@ docString ← match docCommentStx.getOptional? with
   | none   => pure none
   | some s => match s.getArg 1 with
     | Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2)))
-    | _                 => throwError s ("unexpected doc string " ++ toString (s.getArg 1));
+    | _                 => throwErrorAt s ("unexpected doc string " ++ toString (s.getArg 1));
 visibility ← match visibilityStx.getOptional? with
   | none   => pure Visibility.regular
   | some v =>
     let kind := v.getKind;
     if kind == `Lean.Parser.Command.private then pure Visibility.private
     else if kind == `Lean.Parser.Command.protected then pure Visibility.protected
-    else throwError v "unexpected visibility modifier";
+    else throwErrorAt v "unexpected visibility modifier";
 attrs ← match attrsStx.getOptional? with
   | none       => pure #[]
   | some attrs => elabAttrs attrs;
@@ -115,51 +115,51 @@ pure {
   attrs           := attrs
 }
 
-def checkNotAlreadyDeclared (ref : Syntax) (declName : Name) : CommandElabM Unit := do
+def checkNotAlreadyDeclared (declName : Name) : CommandElabM Unit := do
 env ← getEnv;
 when (env.contains declName) $
   match privateToUserName? declName with
-  | none          => throwError ref ("'" ++ declName ++ "' has already been declared")
-  | some declName => throwError ref ("private declaration '" ++ declName ++ "' has already been declared");
+  | none          => throwError ("'" ++ declName ++ "' has already been declared")
+  | some declName => throwError ("private declaration '" ++ declName ++ "' has already been declared");
 when (env.contains (mkPrivateName env declName)) $
-  throwError ref ("a private declaration '" ++ declName ++ "' has already been declared");
+  throwError ("a private declaration '" ++ declName ++ "' has already been declared");
 match privateToUserName? declName with
 | none => pure ()
 | some declName =>
   when (env.contains declName) $
-    throwError ref ("a non-private declaration '" ++ declName ++ "' has already been declared")
+    throwError ("a non-private declaration '" ++ declName ++ "' has already been declared")
 
-def applyVisibility (ref : Syntax) (visibility : Visibility) (declName : Name) : CommandElabM Name :=
+def applyVisibility (visibility : Visibility) (declName : Name) : CommandElabM Name :=
 match visibility with
 | Visibility.private => do
   env ← getEnv;
   let declName := mkPrivateName env declName;
-  checkNotAlreadyDeclared ref declName;
+  checkNotAlreadyDeclared declName;
   pure declName
 | Visibility.protected => do
-  checkNotAlreadyDeclared ref declName;
+  checkNotAlreadyDeclared declName;
   env ← getEnv;
   let env := addProtected env declName;
   setEnv env;
   pure declName
 | _                  => do
-  checkNotAlreadyDeclared ref declName;
+  checkNotAlreadyDeclared declName;
   pure declName
 
-def mkDeclName (ref : Syntax) (modifiers : Modifiers) (atomicName : Name) : CommandElabM Name := do
+def mkDeclName (modifiers : Modifiers) (atomicName : Name) : CommandElabM Name := do
 currNamespace ← getCurrNamespace;
 let declName := currNamespace ++ atomicName;
-applyVisibility ref modifiers.visibility declName
+applyVisibility modifiers.visibility declName
 
-def applyAttributes (ref : Syntax) (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : CommandElabM Unit :=
+def applyAttributes (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : CommandElabM Unit :=
 attrs.forM $ fun attr => do
  env ← getEnv;
  match getAttributeImpl env attr.name with
- | Except.error errMsg => throwError ref errMsg
+ | Except.error errMsg => throwError errMsg
  | Except.ok attrImpl  =>
    when (attrImpl.applicationTime == applicationTime) $ do
      env ← getEnv;
-     env ← liftIO ref $ attrImpl.add env declName attr.args true;
+     env ← liftIO $ attrImpl.add env declName attr.args true;
      setEnv env
 
 end Command
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 406226f5ca..e2d94e45ec 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -59,7 +59,7 @@ let (binders, type) := expandDeclSig (stx.getArg 2);
 let modifiers       := modifiers.addAttribute { name := `instance };
 declId ← match (stx.getArg 1).getOptional? with
   | some declId => pure declId
-  | none        => throwError stx "not implemented yet";
+  | none        => throwError "not implemented yet";
 elabDefLike {
   ref := stx, kind := DefKind.def, modifiers := modifiers,
   declId := declId, binders := binders, type? := type, val := stx.getArg 3
@@ -81,8 +81,8 @@ let declId             := stx.getArg 1;
 let (binders, typeStx) := expandDeclSig (stx.getArg 2);
 scopeLevelNames ← getLevelNames;
 withDeclId declId $ fun name => do
-  declName          ← mkDeclName declId modifiers name;
-  applyAttributes stx declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
+  declName          ← mkDeclName modifiers name;
+  applyAttributes declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
   allUserLevelNames ← getLevelNames;
   decl ← runTermElabM declName $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do {
     type ← Term.elabType typeStx;
@@ -103,8 +103,8 @@ withDeclId declId $ fun name => do
       }
     };
   addDecl decl;
-  applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
-  applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterCompilation
+  applyAttributes declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
+  applyAttributes declName modifiers.attrs AttributeApplicationTime.afterCompilation
 
 /-
 parser! "inductive " >> declId >> optDeclSig >> many ctor
@@ -113,23 +113,23 @@ parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
 Remark: numTokens == 1 for regular `inductive` and 2 for `class inductive`.
 -/
 private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (numTokens := 1) : CommandElabM InductiveView := do
-checkValidInductiveModifier decl modifiers;
+checkValidInductiveModifier modifiers;
 let (binders, type?) := expandOptDeclSig (decl.getArg (numTokens + 1));
 let declId           := decl.getArg numTokens;
 withDeclId declId fun name => do
   levelNames ← getLevelNames;
-  declName   ← mkDeclName declId modifiers name;
-  ctors      ← (decl.getArg (numTokens + 2)).getArgs.mapM fun ctor => do {
+  declName   ← mkDeclName modifiers name;
+  ctors      ← (decl.getArg (numTokens + 2)).getArgs.mapM fun ctor => withRef ctor do {
     -- def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
     ctorModifiers ← elabModifiers (ctor.getArg 1);
     when (ctorModifiers.isPrivate && modifiers.isPrivate) $
-      throwError ctor "invalid 'private' constructor in a 'private' inductive datatype";
+      throwError "invalid 'private' constructor in a 'private' inductive datatype";
     when (ctorModifiers.isProtected && modifiers.isPrivate) $
-      throwError ctor "invalid 'protected' constructor in a 'private' inductive datatype";
-    checkValidCtorModifier ctor ctorModifiers;
+      throwError "invalid 'protected' constructor in a 'private' inductive datatype";
+    checkValidCtorModifier ctorModifiers;
     let ctorName := ctor.getIdAt 2;
     let ctorName := declName ++ ctorName;
-    ctorName ← applyVisibility (ctor.getArg 2) ctorModifiers.visibility ctorName;
+    ctorName ← withRef (ctor.getArg 2) $ applyVisibility ctorModifiers.visibility ctorName;
     let inferMod := !(ctor.getArg 3).isNone;
     let (binders, type?) := expandOptDeclSig (ctor.getArg 4);
     pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, inferMod := inferMod, binders := binders, type? := type? : CtorView }
@@ -184,7 +184,7 @@ fun stx => do
   else if declKind == `Lean.Parser.Command.structure then
     elabStructure modifiers decl
   else
-    throwError stx "unexpected declaration"
+    throwError "unexpected declaration"
 
 /- Return true if all elements of the mutual-block are inductive declarations. -/
 private def isMutualInductive (stx : Syntax) : Bool :=
@@ -243,7 +243,7 @@ fun stx => do
     if isMutualInductive stx then
       elabMutualInductive (stx.getArg 1).getArgs
     else
-      throwError stx "invalid mutual block"
+      throwError "invalid mutual block"
 
 end Command
 end Elab
diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/Definition.lean
index 56bf88c8b1..cc6b0dc894 100644
--- a/src/Lean/Elab/Definition.lean
+++ b/src/Lean/Elab/Definition.lean
@@ -119,12 +119,12 @@ else if kind == `Lean.Parser.Command.declValEqns then
 else
   Term.throwUnsupportedSyntax
 
-def elabDefLike (view : DefView) : CommandElabM Unit := do
-let ref := view.ref;
+def elabDefLike (view : DefView) : CommandElabM Unit :=
+withRef view.ref do
 scopeLevelNames ← getLevelNames;
 withDeclId view.declId $ fun name => do
-  declName          ← mkDeclName view.declId view.modifiers name;
-  applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration;
+  declName          ← withRef view.declId $ mkDeclName view.modifiers name;
+  applyAttributes declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration;
   allUserLevelNames ← getLevelNames;
   decl? ← runTermElabM declName $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs =>
     match view.type? with
@@ -144,9 +144,9 @@ withDeclId view.declId $ fun name => do
   | none      => pure ()
   | some decl => do
     addDecl decl;
-    applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
+    applyAttributes declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
     compileDecl decl;
-    applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
+    applyAttributes declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Elab.definition;
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 06a61271e7..20f614b947 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -15,24 +15,24 @@ namespace Lean
 namespace Elab
 namespace Command
 
-def checkValidInductiveModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
+def checkValidInductiveModifier (modifiers : Modifiers) : CommandElabM Unit := do
 when modifiers.isNoncomputable $
-  throwError ref "invalid use of 'noncomputable' in inductive declaration";
+  throwError "invalid use of 'noncomputable' in inductive declaration";
 when modifiers.isPartial $
-  throwError ref "invalid use of 'partial' in inductive declaration";
+  throwError "invalid use of 'partial' in inductive declaration";
 unless (modifiers.attrs.size == 0 || (modifiers.attrs.size == 1 && (modifiers.attrs.get! 0).name == `class)) $
-  throwError ref "invalid use of attributes in inductive declaration";
+  throwError "invalid use of attributes in inductive declaration";
 pure ()
 
-def checkValidCtorModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
+def checkValidCtorModifier (modifiers : Modifiers) : CommandElabM Unit := do
 when modifiers.isNoncomputable $
-  throwError ref "invalid use of 'noncomputable' in constructor declaration";
+  throwError "invalid use of 'noncomputable' in constructor declaration";
 when modifiers.isPartial $
-  throwError ref "invalid use of 'partial' in constructor declaration";
+  throwError "invalid use of 'partial' in constructor declaration";
 when modifiers.isUnsafe $
-  throwError ref "invalid use of 'unsafe' in constructor declaration";
+  throwError "invalid use of 'unsafe' in constructor declaration";
 when (modifiers.attrs.size != 0) $
-  throwError ref "invalid use of attributes in constructor declaration";
+  throwError "invalid use of attributes in constructor declaration";
 pure ()
 
 
@@ -490,7 +490,7 @@ decl ← runTermElabM view0.declName $ fun vars => Term.withRef ref $ mkInductiv
 addDecl decl;
 mkAuxConstructions views;
 -- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
-views.forM fun view => applyAttributes ref view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
+views.forM fun view => applyAttributes view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
 pure ()
 
 end Command
diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean
index 01e6ea3047..8a83203921 100644
--- a/src/Lean/Elab/Level.lean
+++ b/src/Lean/Elab/Level.lean
@@ -14,7 +14,7 @@ namespace Level
 structure Context :=
 (fileName   : String)
 (fileMap    : FileMap)
-(cmdPos     : String.Pos)
+(ref        : Syntax)
 (levelNames : List Name)
 
 structure State :=
@@ -24,11 +24,14 @@ structure State :=
 abbrev LevelElabM := ReaderT Context (EStateM Exception State)
 
 instance LevelElabM.MonadLog : MonadPosInfo LevelElabM :=
-{ getCmdPos   := do ctx ← read; pure ctx.cmdPos,
+{ getRef      := do ctx ← read; pure ctx.ref,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
   addContext  := fun msg => pure msg }
 
+@[inline] def withRef {α} (ref : Syntax) (x : LevelElabM α) : LevelElabM α := do
+adaptReader (fun (ctx : Context) => { ctx with ref := replaceRef ref ctx.ref }) x
+
 def mkFreshId : LevelElabM Name := do
 s ← get;
 let id := s.ngen.curr;
@@ -41,7 +44,7 @@ modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
 pure $ mkLevelMVar mvarId
 
 partial def elabLevel : Syntax → LevelElabM Level
-| stx => do
+| stx => withRef stx do
   let kind := stx.getKind;
   if kind == `Lean.Parser.Level.paren then
     elabLevel (stx.getArg 1)
@@ -66,19 +69,19 @@ partial def elabLevel : Syntax → LevelElabM Level
   else if kind == `Lean.Parser.Level.num then do
     match (stx.getArg 0).isNatLit? with
     | some val => pure (Level.ofNat val)
-    | none     => throwError stx "ill-formed universe level syntax"
+    | none     => throwError "ill-formed universe level syntax"
   else if kind == `Lean.Parser.Level.ident then do
     let paramName := stx.getIdAt 0;
     ctx ← read;
-    unless (ctx.levelNames.contains paramName) $ throwError stx ("unknown universe level " ++ paramName);
+    unless (ctx.levelNames.contains paramName) $ throwError ("unknown universe level " ++ paramName);
     pure $ mkLevelParam paramName
   else if kind == `Lean.Parser.Level.addLit then do
     lvl ← elabLevel (stx.getArg 0);
     match (stx.getArg 2).isNatLit? with
     | some val => pure (lvl.addOffset val)
-    | none     => throwError stx "ill-formed universe level syntax"
+    | none     => throwError "ill-formed universe level syntax"
   else
-    throwError stx "unexpected universe level syntax kind"
+    throwError "unexpected universe level syntax kind"
 
 end Level
 
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean
index ea239341a2..b934a67238 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Elab/Log.lean
@@ -9,13 +9,18 @@ import Lean.Elab.Exception
 namespace Lean
 namespace Elab
 
+def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
+match ref.getPos with
+| some _ => ref
+| _      => oldRef
+
 class MonadPosInfo (m : Type → Type) :=
 (getFileMap   : m FileMap)
 (getFileName  : m String)
-(getCmdPos    : m String.Pos)
+(getRef       : m Syntax)
 (addContext   : MessageData → m MessageData)
 
-export MonadPosInfo (getFileMap getFileName getCmdPos)
+export MonadPosInfo (getFileMap getFileName getRef)
 
 class MonadLog (m : Type → Type) extends MonadPosInfo m :=
 (logMessage   : Message → m Unit)
@@ -24,26 +29,24 @@ export MonadLog (logMessage)
 
 variables {m : Type → Type} [Monad m]
 
-def getPosition [MonadPosInfo m] (pos : Option String.Pos := none) : m Position := do
-fileMap ← getFileMap;
-cmdPos ← getCmdPos;
-pure $ fileMap.toPosition (pos.getD cmdPos)
+def getRefPos [MonadPosInfo m] : m String.Pos := do
+ref ← getRef;
+pure $ ref.getPos.getD 0
 
-def mkMessageAt [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) (pos : Option String.Pos := none) : m Message := do
+def getRefPosition [MonadPosInfo m] : m Position := do
+pos ← getRefPos;
+fileMap ← getFileMap;
+pure $ fileMap.toPosition pos
+
+def mkMessageAt [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : m Message := do
 fileMap ← getFileMap;
 fileName ← getFileName;
-cmdPos ← getCmdPos;
-let pos := fileMap.toPosition (pos.getD cmdPos);
+let pos := fileMap.toPosition pos;
 msgData ← MonadPosInfo.addContext msgData;
 pure { fileName := fileName, pos := pos, data := msgData, severity := severity }
 
-def getPos [MonadPosInfo m] (stx : Syntax) : m String.Pos :=
-match stx.getPos with
-| some p => pure p
-| none   => getCmdPos
-
-def mkMessage [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) (stx : Syntax) : m Message := do
-pos ← getPos stx;
+def mkMessage [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) : m Message := do
+pos ← getRefPos;
 mkMessageAt msgData severity pos
 
 def logAt [MonadLog m] (pos : String.Pos) (severity : MessageSeverity) (msgData : MessageData) : m Unit := do
@@ -53,25 +56,21 @@ logMessage msg
 def logInfoAt [MonadLog m] (pos : String.Pos) (msgData : MessageData) : m Unit :=
 logAt pos MessageSeverity.information msgData
 
-def log [MonadLog m] (stx : Syntax) (severity : MessageSeverity) (msgData : MessageData) : m Unit := do
-pos ← getPos stx;
+def log [MonadLog m] (severity : MessageSeverity) (msgData : MessageData) : m Unit := do
+pos ← getRefPos;
 logAt pos severity msgData
 
-def logError [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
-log stx MessageSeverity.error msgData
+def logError [MonadLog m] (msgData : MessageData) : m Unit :=
+log MessageSeverity.error msgData
 
-def logWarning [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
-log stx MessageSeverity.warning msgData
+def logWarning [MonadLog m] (msgData : MessageData) : m Unit :=
+log MessageSeverity.warning msgData
 
-def logInfo [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
-log stx MessageSeverity.information msgData
+def logInfo [MonadLog m] (msgData : MessageData) : m Unit :=
+log MessageSeverity.information msgData
 
-def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do
-msg ← mkMessage msgData MessageSeverity.error ref; throw (Exception.error msg)
-
-def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExcept Exception m] (msgData : MessageData) : m α := do
-cmdPos ← getCmdPos;
-msg ← mkMessageAt msgData MessageSeverity.error cmdPos;
+def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (msgData : MessageData) : m α := do
+msg ← mkMessage msgData MessageSeverity.error;
 throw (Exception.error msg)
 
 end Elab
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 110eeb4a6f..ae61f251f9 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -9,8 +9,8 @@ namespace Lean
 namespace Elab
 namespace Command
 
-private def throwUnknownId (ref : Syntax) (id : Name) : CommandElabM Unit :=
-throwError ref ("unknown identifier '" ++ toString id ++ "'")
+private def throwUnknownId (id : Name) : CommandElabM Unit :=
+throwError ("unknown identifier '" ++ toString id ++ "'")
 
 private def lparamsToMessageData (lparams : List Name) : MessageData :=
 match lparams with
@@ -30,19 +30,19 @@ let (m, id) := match privateToUserName? id : _ → MessageData × Name with
 let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type;
 pure m
 
-private def printDefLike (ref : Syntax) (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (isUnsafe := false) : CommandElabM Unit := do
+private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (isUnsafe := false) : CommandElabM Unit := do
 m ← mkHeader kind id lparams type isUnsafe;
 let m := m ++ " :=" ++ Format.line ++ value;
-logInfo ref m
+logInfo m
 
-private def printAxiomLike (ref : Syntax) (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
+private def printAxiomLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
 m ← mkHeader kind id lparams type isUnsafe;
-logInfo ref m
+logInfo m
 
-private def printQuot (ref : Syntax) (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do
-printAxiomLike ref "Quotient primitive" id lparams type
+private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do
+printAxiomLike "Quotient primitive" id lparams type
 
-private def printInduct (ref : Syntax) (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
+private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
     (ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
 env ← getEnv;
 m ← mkHeader "inductive" id lparams type isUnsafe;
@@ -53,28 +53,28 @@ m ← ctors.foldlM
     | some v => pure $ m ++ Format.line ++ ctor ++ " : " ++ v.type
     | none   => pure m)
   m;
-logInfo ref m
+logInfo m
 
-private def printIdCore (ref : Syntax) (id : Name) : CommandElabM Unit := do
+private def printIdCore (id : Name) : CommandElabM Unit := do
 env ← getEnv;
 match env.find? id with
-| ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike ref "axiom" id us t u
-| ConstantInfo.defnInfo  { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike ref "def" id us t v u
-| ConstantInfo.thmInfo  { lparams := us, type := t, value := v, .. } => printDefLike ref "theorem" id us t v.get
-| ConstantInfo.opaqueInfo  { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike ref "constant" id us t u
-| ConstantInfo.quotInfo  { kind := kind, lparams := us, type := t, .. } => printQuot ref kind id us t
-| ConstantInfo.ctorInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike ref "constructor" id us t u
-| ConstantInfo.recInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike ref "recursor" id us t u
+| ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
+| ConstantInfo.defnInfo  { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike "def" id us t v u
+| ConstantInfo.thmInfo  { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v.get
+| ConstantInfo.opaqueInfo  { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u
+| ConstantInfo.quotInfo  { kind := kind, lparams := us, type := t, .. } => printQuot kind id us t
+| ConstantInfo.ctorInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
+| ConstantInfo.recInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
 | ConstantInfo.inductInfo { lparams := us, nparams := nparams, nindices := nindices, type := t, ctors := ctors, isUnsafe := u, .. } =>
-  printInduct ref id us nparams nindices t ctors u
-| none => throwUnknownId ref id
+  printInduct id us nparams nindices t ctors u
+| none => throwUnknownId id
 
-private def printId (ref : Syntax) (id : Name) : CommandElabM Unit := do
+private def printId (id : Name) : CommandElabM Unit := do
 cs ← liftTermElabM none $ Term.resolveGlobalName id;
 let cs := cs.filter fun ⟨_, ps⟩ => ps.isEmpty;
 let cs := cs.map fun ⟨c, _⟩ => c;
-when cs.isEmpty $ throwUnknownId ref id;
-cs.forM fun c => printIdCore ref c
+when cs.isEmpty $ throwUnknownId id;
+cs.forM fun c => printIdCore c
 
 @[builtinCommandElab «print»] def elabPrint : CommandElab :=
 fun stx =>
@@ -82,12 +82,12 @@ fun stx =>
   if numArgs == 2 then
     let arg := stx.getArg 1;
     if arg.isIdent then
-      printId stx arg.getId
+      printId arg.getId
     else match arg.isStrLit? with
-      | some val => logInfo stx val
-      | none     => throwError stx "WIP"
+      | some val => logInfo val
+      | none     => throwError "WIP"
   else
-    throwError stx "invalid #print command"
+    throwError "invalid #print command"
 
 end Command
 end Elab
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index a4603431c4..c5ce162672 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -411,7 +411,7 @@ structure OldContext :=
 (open_nss : List Name)
 
 private def oldRunTermElabM {α} (ctx : OldContext) (x : TermElabM α) : Except String α := do
-match x {fileName := "foo", fileMap := FileMap.ofString "", cmdPos := 0,
+match x {fileName := "foo", fileMap := FileMap.ofString "",
   currNamespace := ctx.env.getNamespace, currRecDepth := 0, maxRecDepth := 10000,
   openDecls := ctx.open_nss.map $ fun n => OpenDecl.simple n [],
   lctx := ctx.locals.foldl (fun lctx l => LocalContext.mkLocalDecl lctx l l exprPlaceholder) $ LocalContext.mkEmpty ()}
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index e2dd93d811..068ee1b9ab 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -100,31 +100,32 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
 let optCtor := structStx.getArg 6;
 if optCtor.isNone then
   pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName := structDeclName ++ defaultCtorName }
-else do
+else
   let ctor := optCtor.getArg 0;
+  withRef ctor do
   ctorModifiers ← elabModifiers (ctor.getArg 0);
-  checkValidCtorModifier ctor ctorModifiers;
+  checkValidCtorModifier ctorModifiers;
   when (ctorModifiers.isPrivate && structModifiers.isPrivate) $
-    throwError ctor "invalid 'private' constructor in a 'private' structure";
+    throwError "invalid 'private' constructor in a 'private' structure";
   when (ctorModifiers.isProtected && structModifiers.isPrivate) $
-    throwError ctor "invalid 'protected' constructor in a 'private' structure";
+    throwError "invalid 'protected' constructor in a 'private' structure";
   let inferMod := !(ctor.getArg 2).isNone;
   let name := ctor.getIdAt 1;
   let declName := structDeclName ++ name;
-  declName ← applyVisibility ctor ctorModifiers.visibility declName;
+  declName ← applyVisibility ctorModifiers.visibility declName;
   pure { ref := ctor, name := name, modifiers := ctorModifiers, inferMod := inferMod, declName := declName }
 
-def checkValidFieldModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
+def checkValidFieldModifier (modifiers : Modifiers) : CommandElabM Unit := do
 when modifiers.isNoncomputable $
-  throwError ref "invalid use of 'noncomputable' in field declaration";
+  throwError "invalid use of 'noncomputable' in field declaration";
 when modifiers.isPartial $
-  throwError ref "invalid use of 'partial' in field declaration";
+  throwError "invalid use of 'partial' in field declaration";
 when modifiers.isUnsafe $
-  throwError ref "invalid use of 'unsafe' in field declaration";
+  throwError "invalid use of 'unsafe' in field declaration";
 when (modifiers.attrs.size != 0) $
-  throwError ref "invalid use of attributes in field declaration";
+  throwError "invalid use of attributes in field declaration";
 when modifiers.isPrivate $
-  throwError ref "private fields are not supported yet";
+  throwError "private fields are not supported yet";
 pure ()
 
 /-
@@ -138,19 +139,19 @@ def structFields         := parser! many (structExplicitBinder <|> structImplici
 private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
 let fieldBinders := ((structStx.getArg 7).getArg 0).getArgs;
 fieldBinders.foldlM
-  (fun (views : Array StructFieldView) fieldBinder => do
+  (fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
     let k := fieldBinder.getKind;
     binfo ←
       if k == `Lean.Parser.Command.structExplicitBinder then pure BinderInfo.default
       else if k == `Lean.Parser.Command.structImplicitBinder then pure BinderInfo.implicit
       else if k == `Lean.Parser.Command.structInstBinder then pure BinderInfo.instImplicit
-      else throwError fieldBinder "unexpected kind of structure field";
+      else throwError "unexpected kind of structure field";
     fieldModifiers ← elabModifiers (fieldBinder.getArg 0);
-    checkValidFieldModifier fieldBinder fieldModifiers;
+    checkValidFieldModifier fieldModifiers;
     when (fieldModifiers.isPrivate && structModifiers.isPrivate) $
-      throwError fieldBinder "invalid 'private' field in a 'private' structure";
+      throwError "invalid 'private' field in a 'private' structure";
     when (fieldModifiers.isProtected && structModifiers.isPrivate) $
-      throwError fieldBinder "invalid 'protected' field in a 'private' structure";
+      throwError "invalid 'protected' field in a 'private' structure";
     let inferMod         := !(fieldBinder.getArg 3).isNone;
     let (binders, type?) :=
       if binfo == BinderInfo.default then
@@ -168,12 +169,12 @@ fieldBinders.foldlM
           some $ (optBinderDefault.getArg 0).getArg 1;
     let idents := (fieldBinder.getArg 2).getArgs;
     idents.foldlM
-      (fun (views : Array StructFieldView) ident => do
+      (fun (views : Array StructFieldView) ident => withRef ident do
         let name     := ident.getId;
         when (isInternalSubobjectFieldName name) $
-          throwError ident ("invalid field name '" ++ name ++ "', identifiers starting with '_' are reserved to the system");
+          throwError ("invalid field name '" ++ name ++ "', identifiers starting with '_' are reserved to the system");
         let declName := structDeclName ++ name;
-        declName ← applyVisibility ident fieldModifiers.visibility declName;
+        declName ← applyVisibility fieldModifiers.visibility declName;
         pure $ views.push {
           ref        := ident,
           modifiers  := fieldModifiers,
@@ -465,11 +466,11 @@ withFields view.fields 0 fieldInfos fun fieldInfos => do
 @[extern "lean_mk_projections"]
 private constant mkProjections (env : Environment) (structName : @& Name) (projs : @& List ProjectionInfo) (isClass : Bool) : Except String Environment := arbitrary _
 
-private def addProjections (ref : Syntax) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : CommandElabM Unit := do
+private def addProjections (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : CommandElabM Unit := do
 env ← getEnv;
 match mkProjections env structName projs isClass with
 | Except.ok env    => setEnv env
-| Except.error msg => throwError ref msg
+| Except.error msg => throwError msg
 
 private def mkAuxConstructions (declName : Name) : CommandElabM Unit := do
 env ← getEnv;
@@ -480,7 +481,7 @@ modifyEnv fun env => mkRecOn env declName;
 when hasUnit $ modifyEnv fun env => mkCasesOn env declName;
 when (hasUnit && hasEq && hasHEq) $ modifyEnv fun env => mkNoConfusion env declName
 
-private def addDefaults (ref : Syntax) (mctx : MetavarContext) (lctx : LocalContext) (localInsts : LocalInstances)
+private def addDefaults (mctx : MetavarContext) (lctx : LocalContext) (localInsts : LocalInstances)
     (defaultAuxDecls : Array (Name × Expr × Expr)) : CommandElabM Unit :=
 liftTermElabM none $ Term.withLocalContext lctx localInsts do
   Term.setMCtx mctx;
@@ -505,7 +506,7 @@ def structCtor           := parser! try (declModifiers >> ident >> optional infe
 
 -/
 def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-checkValidInductiveModifier stx modifiers;
+checkValidInductiveModifier modifiers;
 let isClass   := (stx.getArg 0).getKind == `Lean.Parser.Command.classTk;
 let modifiers := if isClass then modifiers.addAttribute { name := `class } else modifiers;
 let declId    := stx.getArg 1;
@@ -516,7 +517,7 @@ let optType   := stx.getArg 4;
 type ← if optType.isNone then `(Type _) else pure $ (optType.getArg 0).getArg 1;
 scopeLevelNames ← getLevelNames;
 withDeclId declId $ fun name => do
-  declName ← mkDeclName declId modifiers name;
+  declName ← mkDeclName modifiers name;
   allUserLevelNames ← getLevelNames;
   ctor ← expandCtor stx modifiers declName;
   fields ← expandFields stx modifiers declName;
@@ -536,11 +537,11 @@ withDeclId declId $ fun name => do
   };
   let ref := declId;
   addDecl r.decl;
-  addProjections ref declName r.projInfos isClass;
+  addProjections declName r.projInfos isClass;
   mkAuxConstructions declName;
-  applyAttributes ref declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
-  r.projInstances.forM $ addInstance ref;
-  addDefaults ref r.mctx r.lctx r.localInsts r.defaultAuxDecls;
+  applyAttributes declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
+  r.projInstances.forM addInstance;
+  addDefaults r.mctx r.lctx r.localInsts r.defaultAuxDecls;
   pure ()
 
 end Command
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index e8d551b1e5..cbbe58f0fc 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -189,7 +189,7 @@ fun stx => do
   let catName  := stx.getIdAt 1;
   let attrName := catName.appendAfter "Parser";
   env ← getEnv;
-  env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
+  env ← liftIO $ Parser.registerParserCategory env attrName catName;
   setEnv env;
   declareSyntaxCatQuotParser catName
 
@@ -222,7 +222,7 @@ def «syntax»      := parser! "syntax " >> optPrecedence >> optKind >> many1 sy
 fun stx => do
   env ← getEnv;
   let cat := (stx.getIdAt 5).eraseMacroScopes;
-  unless (Parser.isParserCategory env cat) $ throwError (stx.getArg 5) ("unknown category '" ++ cat ++ "'");
+  unless (Parser.isParserCategory env cat) $ throwErrorAt (stx.getArg 5) ("unknown category '" ++ cat ++ "'");
   let prec := (Term.expandOptPrecedence (stx.getArg 1)).getD Parser.maxPrec;
   kind ← elabKind (stx.getArg 2) cat;
   let catParserId := mkIdentFrom stx (cat.appendAfter "Parser");
@@ -232,7 +232,7 @@ fun stx => do
       `(@[$catParserId:ident] def myParser : Lean.TrailingParserDescr := ParserDescr.trailingNode $(quote kind) $(quote prec) $val)
     else
       `(@[$catParserId:ident] def myParser : Lean.ParserDescr := ParserDescr.node $(quote kind) $(quote prec) $val);
-  trace `Elab stx $ fun _ => d;
+  trace `Elab fun _ => d;
   withMacroExpansion stx d $ elabCommand d
 
 /-
@@ -256,13 +256,13 @@ alts ← alts.mapSepElemsM $ fun alt => do {
        pure alt
      else if k' == choiceKind then do
         match quot.getArgs.find? $ fun quotAlt => quotAlt.getKind == k with
-        | none      => throwError alt ("invalid macro_rules alternative, expected syntax node kind '" ++ k ++ "'")
+        | none      => throwErrorAt alt ("invalid macro_rules alternative, expected syntax node kind '" ++ k ++ "'")
         | some quot => do
           pat ← `(`($quot));
           let lhs := lhs.setArg 0 pat;
           pure $ alt.setArg 0 lhs
      else
-       throwError alt ("invalid macro_rules alternative, unexpected syntax node kind '" ++ k' ++ "'")
+       throwErrorAt alt ("invalid macro_rules alternative, unexpected syntax node kind '" ++ k' ++ "'")
   | stx => throwUnsupportedSyntax
 };
 `(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
@@ -275,7 +275,7 @@ match_syntax (alt.getArg 0).getArg 0 with
 def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
 k ← inferMacroRulesAltKind (alts.get! 0);
 if k == choiceKind then
-  throwError (alts.get! 0)
+  throwErrorAt (alts.get! 0)
     "invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
 else do
   altsK    ← alts.filterSepElemsM (fun alt => do k' ← inferMacroRulesAltKind alt; pure $ k == k');
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 852dff5a88..7274403c1f 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -26,7 +26,7 @@ when val.hasExprMVar $ throwError ("tactic failed, result still contain metavari
 def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
 modify $ fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId };
 remainingGoals ← liftTacticElabM mvarId $ do { evalTactic tacticCode; getUnsolvedGoals };
-ref ← getCurrRef;
+ref ← getRef;
 let tailRef := ref.getTailWithPos.getD ref;
 withRef tailRef do
 unless remainingGoals.isEmpty (reportUnsolvedGoals remainingGoals);
@@ -157,8 +157,7 @@ s.syntheticMVars.forM $ fun mvarSyntheticDecl =>
   | SyntheticMVarKind.typeClass =>
     withMVarContext mvarSyntheticDecl.mvarId $ do
       mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId;
-      logError mvarSyntheticDecl.ref $
-        "failed to create type class instance for " ++ indentExpr mvarDecl.type
+      logError $ "failed to create type class instance for " ++ indentExpr mvarDecl.type
   | SyntheticMVarKind.coe expectedType eType e f? =>
     withMVarContext mvarSyntheticDecl.mvarId $ do
       mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId;
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index ff440430a3..1c4fd90000 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -19,7 +19,7 @@ def goalsToMessageData (goals : List MVarId) : MessageData :=
 MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
 
 def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit := do
-ref ← Term.getCurrRef;
+ref ← getRef;
 let tailRef := ref.getTailWithPos.getD ref;
 Term.throwErrorAt tailRef $ "unsolved goals" ++ Format.line ++ goalsToMessageData goals
 
@@ -63,7 +63,7 @@ fun ctx s => match x ctx.toTermCtx s.toTermState with
 def liftMetaM {α} (x : MetaM α) : TacticM α := liftTermElabM $ Term.liftMetaM x
 
 @[inline] def withRef {α} (ref : Syntax) (x : TacticM α) : TacticM α := do
-adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x
+adaptReader (fun (ctx : Context) => { ctx with ref := replaceRef ref ctx.ref }) x
 
 def getEnv : TacticM Environment := do s ← get; pure s.env
 def getMCtx : TacticM MetavarContext := do s ← get; pure s.mctx
@@ -91,7 +91,7 @@ let s := Lean.collectMVars {} e;
 pure s.result.toList
 
 instance monadLog : MonadLog TacticM :=
-{ getCmdPos   := do ctx ← read; pure ctx.cmdPos,
+{ getRef      := do ctx ← read; pure ctx.ref,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
   addContext  := addContext,
@@ -127,7 +127,7 @@ unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) :=
 mkElabAttribute Tactic `Lean.Elab.Tactic.tacticElabAttribute `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic"
 @[init mkTacticAttribute] constant tacticElabAttribute : KeyedDeclsAttribute Tactic := arbitrary _
 
-def logTrace (cls : Name) (ref : Syntax) (msg : MessageData) : TacticM Unit := liftTermElabM $ Term.logTrace cls ref msg
+def logTrace (cls : Name) (msg : MessageData) : TacticM Unit := liftTermElabM $ Term.logTrace cls msg
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : TacticM Unit := liftTermElabM $ Term.trace cls msg
 @[inline] def traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TacticM Unit := liftTermElabM $ Term.traceAtCmdPos cls msg
 def dbgTrace {α} [HasToString α] (a : α) : TacticM Unit :=_root_.dbgTrace (toString a) $ fun _ => pure ()
@@ -316,7 +316,7 @@ fun stx =>
 @[builtinTactic traceState] def evalTraceState : Tactic :=
 fun stx => do
   gs ← getUnsolvedGoals;
-  logInfo stx (goalsToMessageData gs)
+  logInfo (goalsToMessageData gs)
 
 @[builtinTactic «assumption»] def evalAssumption : Tactic :=
 fun stx => liftMetaTactic $ fun mvarId => do Meta.assumption mvarId; pure []
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 2cfce62bfe..b0b6daff87 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -23,7 +23,6 @@ namespace Term
 structure Context extends Meta.Context :=
 (fileName        : String)
 (fileMap         : FileMap)
-(cmdPos          : String.Pos)
 (currNamespace   : Name)
 (declName?       : Option Name     := none)
 (levelNames      : List Name       := [])
@@ -140,7 +139,7 @@ env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
 pure (MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msg)
 
 instance monadLog : MonadLog TermElabM :=
-{ getCmdPos   := do ctx ← read; pure ctx.cmdPos,
+{ getRef      := do ctx ← read; pure ctx.ref,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
   addContext  := addContext,
@@ -148,24 +147,20 @@ instance monadLog : MonadLog TermElabM :=
 
 /- Execute `x` using using `ref` as the default Syntax for providing position information to error messages. -/
 @[inline] def withRef {α} (ref : Syntax) (x : TermElabM α) : TermElabM α := do
-adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x
+adaptReader (fun (ctx : Context) => { ctx with ref := replaceRef ref ctx.ref }) x
 
-def getCurrRef : TermElabM Syntax := do
-ctx ← read; pure ctx.ref
-
-/--
-  Throws an error with the given `msgData` and extracting position information from `ref`.
-  If `ref` does not contain position information, then use `cmdPos` -/
-def throwErrorAt {α} (ref : Syntax) (msgData : MessageData) : TermElabM α := do
+/-- Throws an error with the given `msgData` and extracting position information from `ctx.ref`. -/
+def throwError {α} (msgData : MessageData) : TermElabM α := do
 ctx ← read;
+ref ← getRef;
 let ref     := getBetterRef ref ctx.macroStack;
 let msgData := if ctx.macroStackAtErr then addMacroStack msgData ctx.macroStack else msgData;
-msg ← mkMessage msgData MessageSeverity.error ref;
-throw (Exception.ex (Elab.Exception.error msg))
+withRef ref do
+  msg ← mkMessage msgData MessageSeverity.error;
+  throw (Exception.ex (Elab.Exception.error msg))
 
-def throwError {α} (msgData : MessageData) : TermElabM α := do
-ref ← getCurrRef;
-throwErrorAt ref msgData
+def throwErrorAt {α} (ref : Syntax) (msgData : MessageData) : TermElabM α :=
+withRef ref $ throwError msgData
 
 def throwUnsupportedSyntax {α} : TermElabM α :=
 throw (Exception.ex Elab.Exception.unsupportedSyntax)
@@ -216,17 +211,16 @@ def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := do mctx ← getMCtx
 def assignExprMVar (mvarId : MVarId) (val : Expr) : TermElabM Unit := modify $ fun s => { s with mctx := s.mctx.assignExpr mvarId val }
 def assignLevelMVar (mvarId : MVarId) (val : Level) : TermElabM Unit := modify $ fun s => { s with mctx := s.mctx.assignLevel mvarId val }
 
-def logTrace (cls : Name) (ref : Syntax) (msg : MessageData) : TermElabM Unit := do
+def logTrace (cls : Name) (msg : MessageData) : TermElabM Unit := do
 ctx ← read;
 s   ← get;
-logInfo ref $
+logInfo $
   MessageData.withContext { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts } $
     MessageData.tagged cls msg
 
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : TermElabM Unit := do
 opts ← getOptions;
-ref ← getCurrRef;
-when (checkTraceOption opts cls) $ logTrace cls ref (msg ())
+when (checkTraceOption opts cls) $ logTrace cls (msg ())
 
 def logDbgTrace (msg : MessageData) : TermElabM Unit := do
 trace `Elab.debug $ fun _ => msg
@@ -245,7 +239,8 @@ _root_.dbgTrace (toString a) $ fun _ => pure ()
 
 /-- Auxiliary function for `liftMetaM` -/
 private def mkMessageAux (ctx : Context) (msgData : MessageData) (severity : MessageSeverity) : Message :=
-mkMessageCore ctx.fileName ctx.fileMap msgData severity (ctx.ref.getPos.getD ctx.cmdPos)
+let pos := ctx.ref.getPos.getD 0;
+mkMessageCore ctx.fileName ctx.fileMap msgData severity pos
 
 /-- Auxiliary function for `liftMetaM` -/
 private def fromMetaException (ctx : Context) (ex : Meta.Exception) : Exception :=
@@ -328,7 +323,7 @@ finally x (modify $ fun s => { s with mctx := mctx })
 
 def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
 fun ctx s =>
-  let lvlCtx : Level.Context := { fileName := ctx.fileName, fileMap := ctx.fileMap, cmdPos := ctx.cmdPos, levelNames := ctx.levelNames };
+  let lvlCtx : Level.Context := { fileName := ctx.fileName, fileMap := ctx.fileMap, ref := ctx.ref, levelNames := ctx.levelNames };
   match (x lvlCtx).run { ngen := s.ngen, mctx := s.mctx } with
   | EStateM.Result.ok a newS     => EStateM.Result.ok a { s with mctx := newS.mctx, ngen := newS.ngen }
   | EStateM.Result.error ex newS => EStateM.Result.error (Exception.ex ex) s
@@ -353,7 +348,7 @@ adaptReader (fun (ctx : Context) => { ctx with macroStack := { before := beforeS
   Add the given metavariable to the list of pending synthetic metavariables.
   The method `synthesizeSyntheticMVars` is used to process the metavariables on this list. -/
 def registerSyntheticMVar (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do
-ref ← getCurrRef;
+ref ← getRef;
 modify $ fun s => { s with syntheticMVars := { mvarId := mvarId, ref := ref, kind := kind } :: s.syntheticMVars }
 
 /-
@@ -1287,7 +1282,6 @@ instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
     config        := { opts := opts },
     fileName      := "<TermElabM>",
     fileMap       := arbitrary _,
-    cmdPos        := 0,
     currNamespace := Name.anonymous,
     currRecDepth  := 0,
     maxRecDepth   := getMaxRecDepth opts
diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out
index ccbb94d937..e0f01f5b87 100644
--- a/tests/lean/inductive1.lean.expected.out
+++ b/tests/lean/inductive1.lean.expected.out
@@ -16,9 +16,9 @@ inductive1.lean:49:0: error: invalid mutually inductive types, binder annotation
 inductive1.lean:59:0: error: invalid inductive type, universe parameters mismatch in mutually inductive datatypes
 inductive1.lean:69:2: error: 'Boo.T1.bla' has already been declared
 inductive1.lean:73:10: error: 'Boo.T1' has already been declared
-inductive1.lean:80:8: error: invalid use of 'partial' in inductive declaration
-inductive1.lean:81:14: error: invalid use of 'noncomputable' in inductive declaration
-inductive1.lean:82:10: error: invalid use of attributes in inductive declaration
+inductive1.lean:80:0: error: invalid use of 'partial' in inductive declaration
+inductive1.lean:81:0: error: invalid use of 'noncomputable' in inductive declaration
+inductive1.lean:82:0: error: invalid use of attributes in inductive declaration
 inductive1.lean:85:0: error: invalid 'private' constructor in a 'private' inductive datatype
 inductive1.lean:93:7: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes
 inductive1.lean:100:0: error: constructor resulting type must be specified in inductive family declaration