Skip to content

Commit

Permalink
fix: panic when Syntax.missing
Browse files Browse the repository at this point in the history
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
  • Loading branch information
leodemoura committed Sep 12, 2022
1 parent 506cf01 commit a2631ce
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/Lean/DocString.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit a2631ce

Please sign in to comment.