Remove duplicated position in diagnostics severity 1 (#1322)

This PR fixes issue #1311.
To do so, the position of the error in diagnostics is not included in the message when such error is in the file currently open in the editor.
When the error occurs in a different file ("imported" with `open` command for instance) the position is included in the diagnostic message.
The position is also maintained in the messages printed in the console.
Finally, hover messages are now formatted in Markdown to allow syntax highlighting.

Author: Alidra

CHANGES.md

@@ -8,6 +8,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 ### Changed
 
 - `simplify` now fails if the goal cannot be simplified.
+- Hover messages are now formated in Markdown. Position of the error is removed from diagnostics when the error occurs
+in the file currently open in the editor. 
 
 ## 3.0.0 (2025-07-16)
 

src/lsp/lp_doc.ml

@@ -121,19 +121,20 @@ let process_cmd _file (nodes,st,dg,logs) ast =
 
   | Cmd_Error(loc, msg) ->
     let nodes = { ast; exec = false; goals = [] } :: nodes in
-    let cmd_loc, loc = match cmd_loc, loc with
+    let cmd_loc, loc, diag, log = match cmd_loc, loc with
     | Some l, Some Some l' ->
         if l.fname = l'.fname then
           (* if error in the same file, use the precise location *)
-          Some l', Some l'
+          Some l', Some l', msg, Pos.popt_to_string (Some l') ^ msg
         else
           (* else, use the location of the command *)
-          cmd_loc, Some l'
+          cmd_loc, Some l', Pos.popt_to_string (Some l') ^ "\n" ^ msg
+            , Pos.popt_to_string (Some l') ^ "\n" ^ msg
     (* Otherwise,
       cmd_loc doesn't change and loc is : option_default loc cmd_loc *)
-    | _, Some l' -> cmd_loc, l'
-    | _, None -> cmd_loc, cmd_loc in
-    nodes, st, (cmd_loc, 1, msg, None) :: dg, ((1, msg), loc) :: logs
+    | _, Some l' -> cmd_loc, l', msg, Pos.popt_to_string (l') ^ "\n" ^ msg
+    | _, None -> cmd_loc, cmd_loc, msg, msg in
+    nodes, st, (cmd_loc, 1, diag, None) :: dg, ((1, log), loc) :: logs
 
 let new_doc ~uri ~version ~text =
   let root, logs =

src/lsp/lp_lsp.ml

@@ -450,7 +450,9 @@ let hover_symInfo ofmt ~id params =
     in
     let sym_type = Format.asprintf "%a" Core.Print.sym_type sym_found in
     let result : J.t =
-      `Assoc [ "contents", `String sym_type; "range", range ] in
+      `Assoc [ "contents", `String ("```lambdapi\n" ^ sym_type ^ "\n```");
+        "range", range;
+        "kind", `String "markdown" ] in
     let msg = LSP.mk_reply ~id ~result in
     LIO.send_json ofmt msg
 

src/pure/pure.ml

@@ -159,7 +159,7 @@ let handle_command : state -> Command.t -> command_result =
       in
         Cmd_Proof(ps, d.pdata_proof, d.pdata_sym_pos, d.pdata_end_pos)
   with Fatal(Some p,m) ->
-    Cmd_Error(Some p, Pos.popt_to_string p ^ " " ^ m)
+    Cmd_Error(Some p, m)
 
 let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result =
   fun (_, ss, ps, finalize, prv, sym_pos) tac n ->
@@ -174,7 +174,7 @@ let end_proof : proof_state -> command_result =
   fun (_, ss, ps, finalize, _, _) ->
   try Cmd_OK((Time.save (), finalize ss ps), None)
   with Fatal(Some p,m) ->
-    Cmd_Error(Some p, Pos.popt_to_string p ^ " " ^ m)
+    Cmd_Error(Some p, m)
 
 let get_symbols : state -> Term.sym Extra.StrMap.t =
   fun (_, ss) -> ss.in_scope