From 1e6dadfa5214b0fa2d6edb1494b7eb94accd4b15 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 11 May 2021 17:03:18 +0200
Subject: [PATCH] fix: documentHighlight on partial input

Fixes #455
---
 src/Lean/Server/FileWorker.lean               | 20 ++++++++++---------
 tests/lean/interactive/partialNamespace.lean  |  2 ++
 .../partialNamespace.lean.expected.out        |  9 +++++++++
 3 files changed, 22 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/interactive/partialNamespace.lean
 create mode 100644 tests/lean/interactive/partialNamespace.lean.expected.out

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index a36f15f9fb..3261a9b2f3 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -476,7 +476,7 @@ section RequestHandling
   def hasRange (stx : Syntax) : Bool :=
     stx.getPos?.isSome && stx.getTailPos?.isSome
 
-  def rangeOfSyntax (text : FileMap) (stx : Syntax) : Range :=
+  def rangeOfSyntax! (text : FileMap) (stx : Syntax) : Range :=
     ⟨text.utf8PosToLspPos <| stx.getPos?.get!,
      text.utf8PosToLspPos <| stx.getTailPos?.get!⟩
 
@@ -488,10 +488,10 @@ section RequestHandling
     let rec highlightReturn? (doRange? : Option Range) : Syntax → Option DocumentHighlight
       | stx@`(doElem|return%$i $e) =>
         if stx.getPos?.get! <= pos && pos < stx.getTailPos?.get! then
-          some { range := doRange?.getD (rangeOfSyntax text i), kind? := DocumentHighlightKind.text }
+          some { range := doRange?.getD (rangeOfSyntax! text i), kind? := DocumentHighlightKind.text }
         else
           highlightReturn? doRange? e
-      | `(do%$i $elems) => highlightReturn? (rangeOfSyntax text i) elems
+      | `(do%$i $elems) => highlightReturn? (rangeOfSyntax! text i) elems
       | stx => stx.getArgs.findSome? (highlightReturn? doRange?)
 
     withWaitFindSnap doc (fun s => s.endPos > pos)
@@ -536,8 +536,8 @@ section RequestHandling
               (DocumentSymbol.mk {
                 name := name
                 kind := SymbolKind.method
-                range := rangeOfSyntax text stx
-                selectionRange := rangeOfSyntax text selection
+                range := rangeOfSyntax! text stx
+                selectionRange := rangeOfSyntax! text selection
                } :: syms, stxs')
             else
              (syms, stxs')
@@ -550,11 +550,13 @@ section RequestHandling
           let endStx := match stxs' with
             | endStx::_ => endStx
             | []        => (stx::stxs').getLast!
+          -- we can assume that commands always have at least one position (see `parseCommand`)
+          let range := rangeOfSyntax! text (mkNullNode #[stx, endStx])
           (DocumentSymbol.mk {
-            name := name
-            kind := kind
-            range := ⟨(rangeOfSyntax text stx).start, (rangeOfSyntax text endStx).«end»⟩
-            selectionRange := rangeOfSyntax text selection
+            name
+            kind
+            range
+            selectionRange := if hasRange selection then rangeOfSyntax! text selection else range
             children? := syms.toArray
           } :: syms', stxs'')
 
diff --git a/tests/lean/interactive/partialNamespace.lean b/tests/lean/interactive/partialNamespace.lean
new file mode 100644
index 0000000000..bad8339131
--- /dev/null
+++ b/tests/lean/interactive/partialNamespace.lean
@@ -0,0 +1,2 @@
+namespace
+--^ textDocument/documentSymbol
diff --git a/tests/lean/interactive/partialNamespace.lean.expected.out b/tests/lean/interactive/partialNamespace.lean.expected.out
new file mode 100644
index 0000000000..dba4b7af81
--- /dev/null
+++ b/tests/lean/interactive/partialNamespace.lean.expected.out
@@ -0,0 +1,9 @@
+{"textDocument": {"uri": "file://partialNamespace.lean"},
+ "position": {"line": 0, "character": 2}}
+[{"selectionRange":
+  {"start": {"line": 0, "character": 0}, "end": {"line": 0, "character": 9}},
+  "range":
+  {"start": {"line": 0, "character": 0}, "end": {"line": 0, "character": 9}},
+  "name": "[anonymous]",
+  "kind": 3,
+  "children": []}]