mm0-rs panic

[GinoGiotto]

The following MM1 file causes the mm0-rs LSP server to panic:

delimiter $ ( [ { ~ $ $ } ] ) $;
strict provable sort wff;
term wi (ph ps: wff): wff; infixr wi: $->$ prec 25;
term wn (ph: wff): wff; prefix wn: $~$ prec 41;

axiom ax_1 (ph ps: wff): $ ph -> ps -> ph $;
axiom ax_2 (ph ps ch: wff): $ (ph -> ps -> ch) -> (ph -> ps) -> ph -> ch $;
axiom ax_3 (ph ps: wff): $ (~ph -> ~ps) -> ps -> ph $;
axiom mp (ph ps: wff): $ ph -> ps $ > $ ph $ > $ ps $;

def wa (ph ps: wff): wff = $ ~(ph -> ~ps) $;
infixl wa: $/\$ prec 34;

def wb (ph ps: wff): wff = $ (ph -> ps) /\ (ps -> ph) $;
infixl wb: $<->$ prec 20;

theorem biid (ph: wff): $ ph <-> ph $= 
'(mp (mp ax_3 (mp (mp ax_2 (mp (mp ax_2 (mp (mp ax_2 (mp ax_1 ax_3))
(mp (mp ax_2 (mp ax_1 ax_3)) ax_1))) (! ax_1 _ ph))) (mp ax_1
(mp (mp ax_2 ax_1) (! ax_1 _ ph))))) (mp (mp ax_2 ax_1) (! ax_1 _ ph)));

-- Example theorem with incorrect definition unfolding
theorem _ (ph: wff): $ ph <-> ph $= (fn (refine t)
'(:conv $ ph <-> ph $
 (:unfold wb (ph ph) $ ~((ph -> ph) -> ~(ph -> ph)) $)
,(refine $ ~((ph -> ph) -> ~(ph -> ph)) $ 'biid)));

The origin of the panic seems to be related to the incorrect definition unfolding in the example theorem. The expected unfolding is $ (ph -> ph) /\ (ph -> ph) $, but $ ~((ph -> ph) -> ~(ph -> ph)) $ is provided instead (the panic disappears if the definition unfolding is corrected and the VS Code extension restarted).

The panic error message starts with:

Request textDocument/documentSymbol failed.
Error: Connection got disposed.
...

Lots of text and then finishes with:

...
Server panicked: ServerError(ProtocolError("channel disconnected waiting for exit notification", false))