lambdapi icon indicating copy to clipboard operation
lambdapi copied to clipboard
verified publisher icon Deducteam

Fixing diagnostics

Open Alidra opened this issue 4 months ago • 1 comments

This PR addresses issue https://github.com/Deducteam/lambdapi/issues/1274

  • Messages in the diagnostics are made a bit more expressive.
  • The diagnostic on the ";" at the end of symbol introduction is removed.
  • location of the diagnostic is kept as is on the server side. On the client side (specifically in Emacs) the displayed range is shortened to the three first characters at most of the initial range sent by the server .

Alidra avatar Oct 29 '25 12:10 Alidra

Hi, many thanks for the work on this!

I will test and give my comments when I arrive back to Paris on Monday.

ciaran-matthew-dunne avatar Nov 28 '25 14:11 ciaran-matthew-dunne