From be50f24d64b994c2b6817be592a955258b13d15d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Dec 2019 15:41:02 -0800
Subject: [PATCH] chore: cleanup

---
 src/Init/Lean/Elab/Command.lean | 15 +++------------
 src/Init/Lean/Elab/Log.lean     |  9 +++++++--
 src/Init/Lean/Elab/Term.lean    | 12 +++---------
 3 files changed, 13 insertions(+), 23 deletions(-)

diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 4cd43b2f40..3639e30b91 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -87,18 +87,6 @@ abbrev CommandElabAttribute := ElabAttribute CommandElabTable
 def mkCommandElabAttribute : IO CommandElabAttribute := mkElabAttribute `commandTerm "command" builtinCommandElabTable
 @[init mkCommandElabAttribute] constant commandElabAttribute : CommandElabAttribute := arbitrary _
 
-def throwErrorAt {α} (pos : String.Pos) (msgData : MessageData) : CommandElabM α := do
-ctx ← read;
-throw $ mkExceptionCore ctx.fileName ctx.fileMap msgData pos
-
-def throwError {α} (ref : Syntax) (msgData : MessageData) : CommandElabM α := do
-s ← get;
-throwErrorAt (ref.getPos.getD s.cmdPos) msgData
-
-def throwErrorUsingCmdPos {α} (msgData : MessageData) : CommandElabM α := do
-s ← get;
-throwErrorAt s.cmdPos msgData
-
 def elabCommand (stx : Syntax) : CommandElabM Unit :=
 stx.ifNode
   (fun n => do
@@ -243,6 +231,9 @@ fun stx => do
 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 resolveNamespace (id : Name) : CommandElabM Name := do
 env           ← getEnv;
 currNamespace ← getCurrNamespace;
diff --git a/src/Init/Lean/Elab/Log.lean b/src/Init/Lean/Elab/Log.lean
index 1c10bfcf7e..a7e4c8df74 100644
--- a/src/Init/Lean/Elab/Log.lean
+++ b/src/Init/Lean/Elab/Log.lean
@@ -61,8 +61,13 @@ log stx MessageSeverity.warning msgData
 def logInfo (stx : Syntax) (msgData : MessageData) : m Unit :=
 log stx MessageSeverity.information msgData
 
-def logUnknownDecl (stx : Syntax) (declName : Name) : m Unit :=
-logError stx ("unknown declaration '" ++ toString declName ++ "'")
+def throwError {α} [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do
+msg ← mkMessage msgData MessageSeverity.error ref; throw msg
+
+def throwErrorUsingCmdPos {α} [MonadExcept Exception m] (msgData : MessageData) : m α := do
+cmdPos ← getCmdPos;
+msg ← mkMessageAt msgData MessageSeverity.error cmdPos;
+throw msg
 
 end Elab
 end Lean
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 78fde3e1fa..f86eeb068e 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -143,18 +143,15 @@ instance tracer : SimpleMonadTracerAdapter TermElabM :=
 def dbgTrace {α} [HasToString α] (a : α) : TermElabM Unit :=
 _root_.dbgTrace (toString a) $ fun _ => pure ()
 
-def mkMessage (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
+private def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
 mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
 
-def mkException (ctx : Context) (ref : Syntax) (msgData : MessageData) : Exception :=
-mkMessage ctx ref msgData MessageSeverity.error
-
 private def fromMetaException (ctx : Context) (ref : Syntax) (ex : Meta.Exception) : Exception :=
-mkException ctx ref ex.toMessageData
+mkMessageAux ctx ref ex.toMessageData MessageSeverity.error
 
 private def fromMetaState (ref : Syntax) (ctx : Context) (s : State) (newS : Meta.State) (oldTraceState : TraceState) : State :=
 let traces   := newS.traceState.traces;
-let messages := traces.foldl (fun (messages : MessageLog) trace => messages.add (mkMessage ctx ref trace MessageSeverity.information)) s.messages;
+let messages := traces.foldl (fun (messages : MessageLog) trace => messages.add (mkMessageAux ctx ref trace MessageSeverity.information)) s.messages;
 { toState  := { traceState := oldTraceState, .. newS },
   messages := messages,
   .. s }
@@ -187,9 +184,6 @@ def trySynthInstance (ref : Syntax) (type : Expr) : TermElabM (LOption Expr) :=
 def registerSyntheticMVar (mvarId : MVarId) (ref : Syntax) (kind : SyntheticMVarKind) : TermElabM Unit :=
 modify $ fun s => { syntheticMVars := { mvarId := mvarId, ref := ref, kind := kind } :: s.syntheticMVars, .. s }
 
-def throwError {α} (ref : Syntax) (msgData : MessageData) : TermElabM α := do
-ctx ← read; throw $ mkException ctx ref msgData
-
 @[inline] def withoutPostponing {α} (x : TermElabM α) : TermElabM α :=
 adaptReader (fun (ctx : Context) => { mayPostpone := false, .. ctx }) x