From 95cb76ddb7a65ad4c158034ea62ae343f6d03050 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 14 Oct 2020 17:44:06 -0700
Subject: [PATCH] chore: move to new frontend

---
 src/Lean/Elab/Exception.lean | 29 ++++++++---------------------
 1 file changed, 8 insertions(+), 21 deletions(-)

diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean
index 5487038638..7775c769e8 100644
--- a/src/Lean/Elab/Exception.lean
+++ b/src/Lean/Elab/Exception.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,23 +7,10 @@ Authors: Leonardo de Moura
 import Lean.InternalExceptionId
 import Lean.Meta.Exception
 
-namespace Lean
-namespace Elab
-
-def registerPostponeId : IO InternalExceptionId :=
-registerInternalExceptionId `postpone
-@[init registerPostponeId]
-constant postponeExceptionId : InternalExceptionId := arbitrary _
-
-def registerUnsupportedSyntaxId : IO InternalExceptionId :=
-registerInternalExceptionId `unsupportedSyntax
-@[init registerUnsupportedSyntaxId]
-constant unsupportedSyntaxExceptionId : InternalExceptionId := arbitrary _
-
-def registerAbortElabId : IO InternalExceptionId :=
-registerInternalExceptionId `abortElab
-@[init registerAbortElabId]
-constant abortExceptionId : InternalExceptionId := arbitrary _
+namespace Lean.Elab
+initialize postponeExceptionId : InternalExceptionId ← registerInternalExceptionId `postpone
+initialize unsupportedSyntaxExceptionId : InternalExceptionId ← registerInternalExceptionId `unsupportedSyntax
+initialize abortExceptionId : InternalExceptionId ← registerInternalExceptionId `abortElab
 
 def throwPostpone {α m} [MonadExceptOf Exception m] : m α :=
 throw $ Exception.internal postponeExceptionId
@@ -34,15 +22,14 @@ def throwIllFormedSyntax {α m} [Monad m] [MonadExceptOf Exception m] [Ref m] [A
 throwError "ill-formed syntax"
 
 def throwAlreadyDeclaredUniverseLevel {α m} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (u : Name) : m α :=
-throwError ("a universe level named '" ++ toString u ++ "' has already been declared")
+throwError! "a universe level named '{u}' has already been declared"
 
 -- Throw exception to abort elaboration without producing any error message
 def throwAbort {α m} [MonadExcept Exception m] : m α :=
 throw $ Exception.internal abortExceptionId
 
 def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message :=
-let pos := fileMap.toPosition pos;
+let pos := fileMap.toPosition pos
 { fileName := fileName, pos := pos, data := msgData, severity := severity }
 
-end Elab
-end Lean
+end Lean.Elab