From a2631ce0374220ffdc148e0792b2b1be16ccba59 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 12 Sep 2022 16:10:14 -0700
Subject: [PATCH] fix: panic when `Syntax.missing`

I got a panic error message today in VS Code because of this function.
It is weird because, as far as I can tell, this function is only used by
the `register_simp_attr` macro, and this macro was not being used in
the files I was editing.
I think the fix is resonable for a `Syntax.missing` case.

cc @gebner
---
 src/Lean/DocString.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean
index 70d241e5a2..901e260ff9 100644
--- a/src/Lean/DocString.lean
+++ b/src/Lean/DocString.lean
@@ -95,6 +95,7 @@ def getDocStringText [Monad m] [MonadError m] [MonadRef m] (stx : TSyntax `Lean.
 def TSyntax.getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=
   match stx.raw[1] with
   | Syntax.atom _ val => val.extract 0 (val.endPos - ⟨2⟩)
+  | Syntax.missing    => ""
   | _                 => panic! s!"unexpected doc string\n{stx.raw[1]}"
 
 end Lean