chore: reduce code duplication

src/Init/Lean/Elab/Command.lean

@@ -93,37 +93,13 @@ instance CommandElabM.monadLog : MonadLog CommandElabM :=
   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 -/
-private def getBetterRef (ref : Syntax) : CommandElabM Syntax :=
-match ref.getPos with
-| some _ => pure ref
-| none   => do
-  ctx ← read;
-  match ctx.macroStack.find? $ fun (macro : Syntax) => macro.getPos != none with
-  | some macro => pure macro
-  | none       => pure ref
-
-private def prettyPrint (stx : Syntax) : CommandElabM Format :=
-match stx.reprint with -- TODO use syntax pretty printer
-| some str => pure $ format str.toFormat
-| none     => pure $ format stx
-
-private def addMacroStack (msgData : MessageData) : CommandElabM MessageData := do
-ctx ← read;
-if ctx.macroStack.isEmpty then pure msgData
-else
-  ctx.macroStack.foldlM
-    (fun (msgData : MessageData) (macro : Syntax) => do
-      macroFmt ← prettyPrint macro;
-      pure (msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ macroFmt)))
-    msgData
-
 /--
   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
-ref ← getBetterRef ref;
-msgData ← addMacroStack msgData;
+ctx ← read;
+let ref     := getBetterRef ref ctx.macroStack;
+let msgData := addMacroStack msgData ctx.macroStack;
 msg ← mkMessage msgData MessageSeverity.error ref;
 throw (Exception.error msg)
 
@@ -200,7 +176,7 @@ adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. c
 
 private def elabCommandUsing (stx : Syntax) : List CommandElab → CommandElabM Unit
 | []                => do
-  refFmt ← prettyPrint stx;
+  let refFmt := stx.prettyPrint;
   throwError stx ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
 | (elabFn::elabFns) => catch (elabFn stx)
   (fun ex => match ex with

src/Init/Lean/Elab/Term.lean

@@ -120,37 +120,13 @@ instance TermElabM.MonadLog : MonadLog TermElabM :=
   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 -/
-private def getBetterRef (ref : Syntax) : TermElabM Syntax :=
-match ref.getPos with
-| some _ => pure ref
-| none   => do
-  ctx ← read;
-  match ctx.macroStack.find? $ fun (macro : Syntax) => macro.getPos != none with
-  | some macro => pure macro
-  | none       => pure ref
-
-private def prettyPrint (stx : Syntax) : TermElabM Format :=
-match stx.reprint with -- TODO use syntax pretty printer
-| some str => pure $ str.toFormat
-| none     => pure $ format stx
-
-private def addMacroStack (msgData : MessageData) : TermElabM MessageData := do
-ctx ← read;
-if ctx.macroStack.isEmpty then pure msgData
-else
-  ctx.macroStack.foldlM
-    (fun (msgData : MessageData) (macro : Syntax) => do
-      macroFmt ← prettyPrint macro;
-      pure (msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ macroFmt)))
-    msgData
-
 /--
   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) : TermElabM α := do
-ref ← getBetterRef ref;
-msgData ← addMacroStack msgData;
+ctx ← read;
+let ref     := getBetterRef ref ctx.macroStack;
+let msgData := addMacroStack msgData ctx.macroStack;
 msg ← mkMessage msgData MessageSeverity.error ref;
 throw (Exception.ex (Elab.Exception.error msg))
 
@@ -488,7 +464,7 @@ pure mvar
 private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Expr) (errToSorry : Bool) (catchExPostpone : Bool)
     : List TermElab → TermElabM Expr
 | []                => do
-  refFmt ← prettyPrint stx;
+  let refFmt := stx.prettyPrint;
   throwError stx ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
 | (elabFn::elabFns) => catch (elabFn stx expectedType?)
   (fun ex => match ex with

src/Init/Lean/Elab/Util.lean

@@ -8,8 +8,32 @@ import Init.Lean.Util.Trace
 import Init.Lean.Parser
 
 namespace Lean
+
+def Syntax.prettyPrint (stx : Syntax) : Format :=
+match stx.reprint with -- TODO use syntax pretty printer
+| some str => format str.toFormat
+| none     => format stx
+
 namespace Elab
 
+/- If `ref` does not have position information, then try to use macroStack -/
+def getBetterRef (ref : Syntax) (macroStack : List Syntax) : Syntax :=
+match ref.getPos with
+| some _ => ref
+| none   =>
+  match macroStack.find? $ fun (macro : Syntax) => macro.getPos != none with
+  | some macro => macro
+  | none       => ref
+
+def addMacroStack (msgData : MessageData) (macroStack : List Syntax) : MessageData :=
+if macroStack.isEmpty then msgData
+else
+  macroStack.foldl
+    (fun (msgData : MessageData) (macro : Syntax) =>
+      let macroFmt := macro.prettyPrint;
+      msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ macroFmt))
+    msgData
+
 def checkSyntaxNodeKind (env : Environment) (k : Name) : ExceptT String Id Name :=
 if Parser.isValidSyntaxNodeKind env k then pure k
 else throw "failed"
@@ -156,7 +180,5 @@ fun stx =>
 registerTraceClass `Elab;
 registerTraceClass `Elab.step
 
-
-
 end Elab
 end Lean