[coq] Properly concatenate warnings

Thanks to @mituharu for the careful bug report.

Fixes #540

CHANGES.md

@@ -5,6 +5,8 @@
    improvements to goal pretty printing (@ejgallego, #530)
  - Added link to Python coq-lsp client by Pedro Carrot and Nuno
    Saavedra (@Nfsaavedra, #536)
+ - Properly concatenate warnings from _CoqProject (@ejgallego,
+   reported by @mituharu, #541, fixes #540)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

coq/workspace.ml

@@ -34,16 +34,18 @@ module Warning : sig
   type t
 
   val make : string -> t
-  val apply : t -> unit
+
+  (** Adds new warnings to the list of current warnings *)
+  val apply : t list -> unit
 end = struct
   type t = string
 
   let make x = x
-  let to_string x = x
 
   let apply w =
-    let warn = CWarnings.get_flags () in
-    CWarnings.set_flags (warn ^ to_string w)
+    let old_warn = CWarnings.get_flags () in
+    let new_warn = String.concat "," w in
+    CWarnings.set_flags (old_warn ^ "," ^ new_warn)
 end
 
 type t =
@@ -236,7 +238,7 @@ let apply ~uri
     } =
   if debug then CDebug.set_flags "backtrace";
   Flags.apply flags;
-  List.iter Warning.apply warnings;
+  Warning.apply warnings;
   List.iter Mltop.add_ml_dir ml_include_path;
   findlib_init ~ml_include_path ~ocamlpath;
   List.iter Loadpath.add_vo_path vo_load_path;

coq/workspace.mli

@@ -26,7 +26,10 @@ module Warning : sig
   type t
 
   val make : string -> t
-  val apply : t -> unit
+
+  (** Adds new warnings to the list of current warnings, the Coq API
+      here is a bit tricky... *)
+  val apply : t list -> unit
 end
 
 type t = private

test/CoqProject/_CoqProject

@@ -2,5 +2,6 @@
 -Q . test
 
 -arg -w -arg -local-declaration
+-arg -w -arg +non-primitive-record
 
 test.v

test/CoqProject/test.v

@@ -1 +1,7 @@
 Variable (A : nat).
+
+Set Primitive Projections.
+
+Record a := { _ : nat }.
+
+Print Options.