From 8b66dbf28523df142ef3dbc4ed5245924216344f Mon Sep 17 00:00:00 2001 From: tydeu Date: Sat, 11 Dec 2021 17:53:31 -0500 Subject: [PATCH] refactor: use `error` in `Load.lean` --- Lake/Config/Load.lean | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index 9859df51f3..ab25db274c 100644 --- a/Lake/Config/Load.lean +++ b/Lake/Config/Load.lean @@ -29,9 +29,8 @@ unsafe def evalPackageDecl (env : Environment) (declName : Name) let m := env.evalConstCheck PackageConfig leanOpts ``PackageConfig declName if let Except.ok config := m.run.run then return config - throw <| IO.userError <| - s!"unexpected type at `{declName}`, " ++ - "`Lake.IOPackager`, `Lake.Packager`, or `Lake.PackageConfig` expected" + error <| s!"unexpected type at `{declName}`, " ++ + "`Lake.IOPackager`, `Lake.Packager`, or `Lake.PackageConfig` expected" /-- Evaluate a `script` declaration to its respective `Script`. -/ unsafe def evalScriptDecl @@ -50,19 +49,15 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) let (env, ok) ← Elab.runFrontend input leanOpts configFile.toString configModName if ok then match packageAttr.ext.getState env |>.toList with - | [] => - throw <| IO.userError - s!"configuration file is missing a `package` declaration" + | [] => error s!"configuration file is missing a `package` declaration" | [pkgDeclName] => let config ← evalPackageDecl env pkgDeclName dir args leanOpts let scripts ← scriptAttr.ext.getState env |>.foldM (init := {}) fun m d => do m.insert d <| ← evalScriptDecl env d leanOpts return {dir, config, scripts} - | _ => - throw <| IO.userError - s!"configuration file has multiple `package` declarations" + | _ => error s!"configuration file has multiple `package` declarations" else - throw <| IO.userError s!"package configuration `{configFile}` has errors" + error s!"package configuration `{configFile}` has errors" /-- Load the package located in