26 april 2023 20:58:45 UTC+2 Glauco wrote:
(DISCLAIMER: while writing formulas, now and then, there's some slowdown because the language server is sending a superlong error diagnostic for every character you type: I will leave this as a "verbose" non default option, but a shorter diagnostic message should fix it) I've just published ver.0.0.4 that has a new configuration parameter for the diagnostic message, for theory's formula syntax errors: - "short" (default) does not slow down typing - "verbose" gives full details about the expected characters and why the theory grammar requires them (for large grammars, it could slow down typing, since the diagnostic is sent for every character) Glauco -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/968a8d7c-f418-494f-83b7-aa49f1601fden%40googlegroups.com.
