From be33ca69cddf21f2475cb7394e0d8a7aca54dc0a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 10 Jan 2021 08:30:14 -0800
Subject: [PATCH] feat: environment extension for storing declaration ranges

---
 src/Lean.lean                  |  1 +
 src/Lean/DeclarationRange.lean | 28 ++++++++++++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 src/Lean/DeclarationRange.lean

diff --git a/src/Lean.lean b/src/Lean.lean
index 507c58be16..d5e58563dc 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -28,3 +28,4 @@ import Lean.InternalExceptionId
 import Lean.Server
 import Lean.ScopedEnvExtension
 import Lean.DocString
+import Lean.DeclarationRange
diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean
new file mode 100644
index 0000000000..f142f1ae63
--- /dev/null
+++ b/src/Lean/DeclarationRange.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.MonadEnv
+
+namespace Lean
+
+structure DeclarationRange where
+  pos    : Position
+  endPos : Position
+  deriving Inhabited, DecidableEq
+
+structure DeclarationRanges where
+  range          : DeclarationRange
+  selectionRange : DeclarationRange
+  deriving Inhabited
+
+builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension `declranges
+
+def addDeclarationRanges [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) : m Unit :=
+  modifyEnv fun env => declRangeExt.insert env declName declRanges
+
+def findDeclarationRanges? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
+  return declRangeExt.find? (← getEnv) declName
+
+end Lean