From 6a3f065948107ae31e5df433871e975752175344 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Thu, 12 Dec 2024 11:56:52 +0100 Subject: [PATCH] Improve diagnostic messages --- server/lib/why3findUtil.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/server/lib/why3findUtil.ml b/server/lib/why3findUtil.ml index 3a7bf3b..581c47e 100644 --- a/server/lib/why3findUtil.ml +++ b/server/lib/why3findUtil.ml @@ -533,8 +533,8 @@ let diagnostics_of_info info : Diagnostic.t list = let open ProofInfo in let mk_diagnostic goal = let range = Option.value ~default:info.entity_range goal.range in - let message = Printf.sprintf "Unproved %s" goal.expl in - Diagnostic.create ~range ~severity:DiagnosticSeverity.Error ~message () + let message = Printf.sprintf "Unproved goal: %s" goal.expl in + Diagnostic.create ~source:"Creusot" ~range ~severity:DiagnosticSeverity.Error ~message () in List.map mk_diagnostic info.unproved_goals