[fix] diag msg

This commit is contained in:
Andy Bunce 2025-08-19 15:20:44 +01:00
parent ba9a3594b0
commit 6829f17673
4 changed files with 36 additions and 28 deletions

View file

@ -56,7 +56,8 @@ document.getElementById("load").onchange = e => {
insert: t
}
})
console.log("SYNC")
client.sync();
console.log("SYNC");
});
document.getElementById("load").value="";
};
@ -104,11 +105,11 @@ function diags(params){
const severities=["error","warning" ,"info","hint" ]
//
const diagnostics = params.diagnostics
.map(({ range, message, severity }) => ({
.map(({ range, message, severity,code }) => ({
from: plugin.fromPosition( range.start,view.state.doc),
to: plugin.fromPosition( range.end,view.state.doc),
severity: severities[severity -1],
message,
message: ((typeof code === 'undefined')?"":`[${code}] `)+message,
}))
.filter(
({ from, to }) =>