From 1be41f2adbcbbc6a7cdeeeebbba2dc605dc8842e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Aug 2021 12:58:58 -0700
Subject: [PATCH] chore: fix stdlib

---
 src/Lean/Elab/Quotation.lean   |  6 ++++--
 src/Lean/Server/InfoUtils.lean | 17 +++++++++--------
 src/Leanpkg/Manifest.lean      |  2 +-
 3 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 1687eea006..34716cc4dd 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -32,8 +32,10 @@ private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermEl
   | stx => pure stx
 
 private def getSepFromSplice (splice : Syntax) : Syntax := do
-  let Syntax.atom _ sep ← getAntiquotSpliceSuffix splice | unreachable!
-  Syntax.mkStrLit (sep.dropRight 1)
+  if let Syntax.atom _ sep := getAntiquotSpliceSuffix splice then
+    Syntax.mkStrLit (sep.dropRight 1)
+  else
+    unreachable!
 
 partial def mkTuple : Array Syntax → TermElabM Syntax
   | #[]  => `(Unit.unit)
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 03452a8066..487b62e58e 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -195,14 +195,15 @@ structure GoalsAtResult where
 partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult := do
   t.deepestNodes fun
     | ctx, i@(Info.ofTacticInfo ti), cs => OptionM.run do
-      let (some pos, some tailPos) ← pure (i.pos?, i.tailPos?)
-        | failure
-      let trailSize := i.stx.getTrailingSize
-      -- show info at EOF even if strictly outside token + trail
-      let atEOF := tailPos == text.source.bsize
-      guard <| pos ≤ hoverPos ∧ (hoverPos < tailPos + trailSize || atEOF)
-      return { ctxInfo := ctx, tacticInfo := ti, useAfter :=
-        hoverPos > pos && (hoverPos >= tailPos || !cs.any (hasNestedTactic pos tailPos)) }
+      if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
+        let trailSize := i.stx.getTrailingSize
+        -- show info at EOF even if strictly outside token + trail
+        let atEOF := tailPos == text.source.bsize
+        guard <| pos ≤ hoverPos ∧ (hoverPos < tailPos + trailSize || atEOF)
+        return { ctxInfo := ctx, tacticInfo := ti, useAfter :=
+          hoverPos > pos && (hoverPos >= tailPos || !cs.any (hasNestedTactic pos tailPos)) }
+      else
+        failure
     | _, _, _ => none
 where
   hasNestedTactic (pos tailPos) : InfoTree → Bool
diff --git a/src/Leanpkg/Manifest.lean b/src/Leanpkg/Manifest.lean
index 50caaafe4e..e993564abb 100644
--- a/src/Leanpkg/Manifest.lean
+++ b/src/Leanpkg/Manifest.lean
@@ -16,7 +16,7 @@ inductive Source where
 
 namespace Source
 
-def fromToml (v : Toml.Value) : Option Source :=
+def fromToml (v : Toml.Value) : OptionM Source :=
   (do let Toml.Value.str dir ← v.lookup "path" | none
       path ⟨dir⟩) <|>
   (do let Toml.Value.str url ← v.lookup "git" | none