Fix location when reporting errors in another file (#1310)

This PR fixes the issue #1299 .
The new solution checks the error is located in the same file.
If not, the error is reported on the import command displaying the location in the imported file

Author: Alidra

src/lsp/lp_doc.ml

@@ -121,8 +121,19 @@ let process_cmd _file (nodes,st,dg,logs) ast =
 
   | Cmd_Error(loc, msg) ->
     let nodes = { ast; exec = false; goals = [] } :: nodes in
-    let loc = option_default loc Command.(get_pos ast) in
-    nodes, st, (loc, 1, msg, None) :: dg, ((1, msg), loc) :: logs
+    let cmd_loc, loc = 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'
+        else
+          (* else, use the location of the command *)
+          cmd_loc, Some l'
+    (* 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
 
 let new_doc ~uri ~version ~text =
   let root, logs =