From 266774409272fd5757365ed1f3761ffffe7b07d4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Apr 2021 18:25:19 -0700
Subject: [PATCH] fix: panic message

---
 src/Lean/Server/FileWorker.lean | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 3b112ae911..e2e7ebb93d 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -471,6 +471,9 @@ section RequestHandling
 
         return none
 
+  def hasRange (stx : Syntax) : Bool :=
+    stx.getPos?.isSome && stx.getTailPos?.isSome
+
   def rangeOfSyntax (text : FileMap) (stx : Syntax) : Range :=
     ⟨text.utf8PosToLspPos <| stx.getPos?.get!,
      text.utf8PosToLspPos <| stx.getTailPos?.get!⟩
@@ -520,19 +523,22 @@ section RequestHandling
         | `(end $(id)?) => ([], stx::stxs)
         | _ =>
           let (syms, stxs') := toDocumentSymbols text stxs
-          if stx.isOfKind ``Lean.Parser.Command.declaration then
+          if stx.isOfKind ``Lean.Parser.Command.declaration && hasRange stx then
             let (name, selection) := match stx with
               | `($dm:declModifiers $ak:attrKind instance $[$np:namedPrio]? $[$id:ident$[.{$ls,*}]?]? $sig:declSig $val) =>
                 ((·.getId.toString) <$> id |>.getD s!"instance {sig.reprint.getD ""}", id.getD sig)
               | _ => match stx[1][1] with
                 | `(declId|$id:ident$[.{$ls,*}]?) => (id.getId.toString, id)
                 | _                               => (stx[1][0].isIdOrAtom?.getD "<unknown>", stx[1][0])
-            (DocumentSymbol.mk {
-              name := name
-              kind := SymbolKind.method
-              range := rangeOfSyntax text stx
-              selectionRange := rangeOfSyntax text selection
-            } :: syms, stxs')
+            if hasRange selection then
+              (DocumentSymbol.mk {
+                name := name
+                kind := SymbolKind.method
+                range := rangeOfSyntax text stx
+                selectionRange := rangeOfSyntax text selection
+               } :: syms, stxs')
+            else
+             (syms, stxs')
           else
             (syms, stxs')
       sectionLikeToDocumentSymbols (text : FileMap) (stx : Syntax) (stxs : List Syntax) (name : String) (kind : SymbolKind) (selection : Syntax) :=