create DocumentLocation

src/Lean/Data/DeclarationRange.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Data.Position
+
+/-!
+# Data types for declaration ranges
+
+The environment extension for declaration ranges is in `Lean.DeclarationRange`.
+-/
+
+namespace Lean
+
+/-- Store position information for declarations. -/
+structure DeclarationRange where
+  pos          : Position
+  /-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this
+  because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode
+  codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source
+  file, which is IO-heavy. -/
+  charUtf16    : Nat
+  endPos       : Position
+  /-- See `charUtf16`. -/
+  endCharUtf16 : Nat
+  deriving Inhabited, DecidableEq, Repr
+
+instance : ToExpr DeclarationRange where
+  toExpr r   := mkAppN (mkConst ``DeclarationRange.mk) #[toExpr r.pos, toExpr r.charUtf16, toExpr r.endPos, toExpr r.endCharUtf16]
+  toTypeExpr := mkConst ``DeclarationRange
+
+structure DeclarationRanges where
+  range          : DeclarationRange
+  selectionRange : DeclarationRange
+  deriving Inhabited, Repr
+
+instance : ToExpr DeclarationRanges where
+  toExpr r   := mkAppN (mkConst ``DeclarationRanges.mk) #[toExpr r.range, toExpr r.selectionRange]
+  toTypeExpr := mkConst ``DeclarationRanges
+
+/--
+A declaration location is a declaration range along with the name of the module the declaration resides in.
+-/
+structure DeclarationLocation where
+  module : Name
+  range : DeclarationRange
+  deriving Inhabited, DecidableEq, Repr

src/Lean/DeclarationRange.lean

@@ -4,37 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Data.DeclarationRange
 import Lean.MonadEnv
-import Lean.AuxRecursor
-import Lean.ToExpr
 
-namespace Lean
+/-!
+# Environment extension for declaration ranges
+-/
 
-/-- Store position information for declarations. -/
-structure DeclarationRange where
-  pos          : Position
-  /-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this
-  because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode
-  codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source
-  file, which is IO-heavy. -/
-  charUtf16    : Nat
-  endPos       : Position
-  /-- See `charUtf16`. -/
-  endCharUtf16 : Nat
-  deriving Inhabited, DecidableEq, Repr
-
-instance : ToExpr DeclarationRange where
-  toExpr r   := mkAppN (mkConst ``DeclarationRange.mk) #[toExpr r.pos, toExpr r.charUtf16, toExpr r.endPos, toExpr r.endCharUtf16]
-  toTypeExpr := mkConst ``DeclarationRange
-
-structure DeclarationRanges where
-  range          : DeclarationRange
-  selectionRange : DeclarationRange
-  deriving Inhabited, Repr
-
-instance : ToExpr DeclarationRanges where
-  toExpr r   := mkAppN (mkConst ``DeclarationRanges.mk) #[toExpr r.range, toExpr r.selectionRange]
-  toTypeExpr := mkConst ``DeclarationRanges
+namespace Lean
 
 builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) ← IO.mkRef {}
 builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension

src/Lean/Elab/InfoTree/Main.lean

@@ -193,7 +193,7 @@ def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"
 
 def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format := do
-  let loc := if let some (module, rng) := info.location? then f!"{module} {rng.start}-{rng.end}" else "none"
+  let loc := if let some loc := info.location? then f!"{loc.module} {loc.range.pos}-{loc.range.endPos}" else "none"
   return f!"DelabTermInfo @ {← TermInfo.format ctx info.toTermInfo}\n\
     Location: {loc}\n\
     Docstring: {repr info.docString?}\n\

src/Lean/Elab/InfoTree/Types.lean

@@ -5,12 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Lean.Data.Position
+import Lean.Data.DeclarationRange
 import Lean.Data.OpenDecl
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Data.Json
-import Lean.Data.Lsp.Basic
 import Lean.Server.Rpc.Basic
 import Lean.Widget.Types
 
@@ -179,8 +178,8 @@ Regular terms are delaborated explicitly, whereas omitted terms are simply to be
 regular delaboration settings. Additionally, omissions come with a reason for omission.
 -/
 structure DelabTermInfo extends TermInfo where
-  /-- A module and source range to use for "go to definition", to override the default. -/
-  location? : Option (Name × Lsp.Range) := none
+  /-- A source position to use for "go to definition", to override the default. -/
+  location? : Option DeclarationLocation := none
   /-- Text to use to override the docstring. -/
   docString? : Option String := none
   /-- Whether to use explicit mode when pretty printing the term on hover. -/

src/Lean/Meta/Sorry.lean

@@ -43,21 +43,24 @@ structure SorryLabelView where
   The logical source position is used when displaying the sorry when the `pp.sorrySource` option is true,
   and the LSP range is used for "go to definition" in the Infoview.
   -/
-  module? : Option (Name × Position × Lsp.Range) := none
+  module? : Option DeclarationLocation := none
 
 def SorryLabelView.encode (view : SorryLabelView) : CoreM Name :=
   let name :=
-    if let some (mod, pos, range) := view.module? then
-      mod |>.num pos.line |>.num pos.column |>.num range.start.line |>.num range.start.character |>.num range.end.line |>.num range.end.character
+    if let some { module, range := { pos, endPos, charUtf16, endCharUtf16 } } := view.module? then
+      module
+        |>.num pos.line |>.num pos.column
+        |>.num endPos.line |>.num endPos.column
+        |>.num charUtf16 |>.num endCharUtf16
     else
       .anonymous
   mkFreshUserName (name.str "_sorry")
 
 def SorryLabelView.decode? (name : Name) : Option SorryLabelView := do
   guard <| name.hasMacroScopes
   let .str name "_sorry" := name.eraseMacroScopes | failure
-  if let .num (.num (.num (.num (.num (.num name posLine) posCol) startLine) startChar) endLine) endChar := name then
-    return { module? := some (name, ⟨posLine, posCol⟩, ⟨⟨startLine, startChar⟩, ⟨endLine, endChar⟩⟩) }
+  if let .num (.num (.num (.num (.num (.num module posLine) posCol) endLine) endCol) charUtf16) endCharUtf16 := name then
+    return { module? := some { module, range := { pos := ⟨posLine, posCol⟩, endPos := ⟨endLine, endCol⟩, charUtf16, endCharUtf16 } } }
   else
     failure
 
@@ -71,11 +74,19 @@ Constructs a `sorryAx`.
 -/
 def mkLabeledSorry (type : Expr) (synthetic : Bool) (unique : Bool) : MetaM Expr := do
   let tag ←
-    if let (some startPos, some endPos) := ((← getRef).getPos?, (← getRef).getTailPos?) then
+    if let (some startSPos, some endSPos) := ((← getRef).getPos?, (← getRef).getTailPos?) then
       let fileMap ← getFileMap
-      let pos := fileMap.toPosition startPos
-      let range := fileMap.utf8RangeToLspRange ⟨startPos, endPos⟩
-      SorryLabelView.encode { module? := (← getMainModule, pos, range) }
+      SorryLabelView.encode {
+        module? := some {
+          module := (← getMainModule)
+          range := {
+            pos := fileMap.toPosition startSPos
+            endPos := fileMap.toPosition endSPos
+            charUtf16 := (fileMap.utf8PosToLspPos startSPos).character
+            endCharUtf16 := (fileMap.utf8PosToLspPos endSPos).character
+          }
+        }
+      }
     else
       SorryLabelView.encode {}
   if unique then

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -212,7 +212,7 @@ where
   }
 
 def addDelabTermInfo (pos : Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false)
-    (location? : Option (Name × Lsp.Range) := none) (docString? : Option String := none) (explicit : Bool := true) : DelabM Unit := do
+    (location? : Option DeclarationLocation := none) (docString? : Option String := none) (explicit : Bool := true) : DelabM Unit := do
   let info := Info.ofDelabTermInfo {
     toTermInfo := ← addTermInfo.mkTermInfo stx e (isBinder := isBinder)
     location?  := location?

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1297,18 +1297,18 @@ def delabSorry : Delab := whenPPOption getPPNotation <| whenNotPPOption getPPExp
   -- But, if `pp.explicit` is false and `pp.sorrySource` is true, then print a simplified version of the tag.
   if let some view := isLabeledSorry? (← getExpr) then
     withOverApp 3 do
-      if let some (module, pos, range) := view.module? then
+      if let some loc := view.module? then
         let (stx, explicit) ←
           if ← pure sorrySource <||> getPPOption getPPSorrySource then
-            let posAsName := Name.mkSimple s!"{module}:{pos.line}:{pos.column}"
+            let posAsName := Name.mkSimple s!"{loc.module}:{loc.range.pos.line}:{loc.range.pos.column}"
             let pos := mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{posAsName}"]
             let src ← withAppArg <| annotateTermInfo pos
             pure (← `(sorry $src), true)
           else
             -- Set `explicit` to false so that the first hover sets `pp.sorrySource` to true in `Lean.Widget.ppExprTagged`
             pure (← `(sorry), false)
         let stx ← annotateCurPos stx
-        addDelabTermInfo (← getPos) stx (← getExpr) (explicit := explicit) (location? := some (module, range))
+        addDelabTermInfo (← getPos) stx (← getExpr) (explicit := explicit) (location? := loc)
           (docString? := "This is a `sorry` term associated to a source position. Use 'Go to definition' to go there.")
         return stx
       else

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -215,8 +215,9 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
   | .ofTermInfo ti =>
     return ← locationLinksFromTermInfo ti
   | .ofDelabTermInfo { toTermInfo := ti, location?, .. } =>
-    if let some (module, range) := location? then
-      if let some targetUri ← documentUriFromModule rc.srcSearchPath module then
+    if let some location := location? then
+      if let some targetUri ← documentUriFromModule rc.srcSearchPath location.module then
+        let range := location.range.toLspRange
         let result : LocationLink := {
           targetUri, targetRange := range, targetSelectionRange := range,
           originSelectionRange? := (·.toLspRange text) <$> i.range?