From fe03e2b5cbac8d54dabce666290684edef69aa89 Mon Sep 17 00:00:00 2001
From: blackbird1128 <37084688+blackbird1128@users.noreply.github.com>
Date: Fri, 15 Nov 2024 17:03:58 +0100
Subject: [PATCH 1/2] Fix the output of the AST dump plugin to be a valid JSON

---
 plugins/astdump/main.ml | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/plugins/astdump/main.ml b/plugins/astdump/main.ml
index ae7ffe848..41e22d39e 100644
--- a/plugins/astdump/main.ml
+++ b/plugins/astdump/main.ml
@@ -1,17 +1,22 @@
 open Fleche
 
-let pp_json fmt (ast : Doc.Node.Ast.t) =
-  Lsp.JCoq.Ast.to_yojson ast.v |> Yojson.Safe.pretty_print fmt
+type outputFormat = Json | Sexp
 
-let pp_sexp fmt (ast : Doc.Node.Ast.t) =
+let ast_to_json (ast : Doc.Node.Ast.t) =
+  Lsp.JCoq.Ast.to_yojson ast.v
+
+let ast_to_sexp_string (ast : Doc.Node.Ast.t) =
   Serlib.Ser_vernacexpr.sexp_of_vernac_control (Coq.Ast.to_coq ast.v)
-  |> Sexplib.Sexp.pp_hum fmt
+  |> Sexplib.Sexp.to_string_hum
 
-let pw pp fmt ast = Format.fprintf fmt "@[%a@]" pp ast
 
-let dump_asts ~out_file pp asts =
-  let f fmt asts = List.iter (pw pp fmt) asts in
-  Coq.Compat.format_to_file ~file:out_file ~f asts
+let dump_asts ~out_file (asts: Doc.Node.Ast.t list) output_format =
+    let out_chan = open_out out_file in
+    match output_format with 
+     Json -> 
+         Yojson.Safe.pretty_to_channel out_chan (`List (List.map ast_to_json asts));
+    | Sexp -> 
+         output_string out_chan  (List.map (fun ast -> ast_to_sexp_string ast) asts |> String.concat "\n")
 
 let dump_ast ~io ~token:_ ~(doc : Doc.t) =
   let uri = doc.uri in
@@ -21,10 +26,10 @@ let dump_ast ~io ~token:_ ~(doc : Doc.t) =
   let asts = Doc.asts doc in
   (* Output json *)
   let out_file_j = Lang.LUri.File.to_string_file uri ^ ".json.astdump" in
-  let () = dump_asts ~out_file:out_file_j pp_json asts in
+  dump_asts ~out_file:out_file_j asts Json;
   (* Output sexp *)
   let out_file_s = Lang.LUri.File.to_string_file uri ^ ".sexp.astdump" in
-  let () = dump_asts ~out_file:out_file_s pp_sexp asts in
+  dump_asts ~out_file:out_file_s asts Sexp;
   Io.Report.msg ~io ~lvl "[ast plugin] dumping ast for %s was completed!"
     uri_str;
   ()

From 56717c269c02ae179f346c636b7b1fa16de35435 Mon Sep 17 00:00:00 2001
From: blackbird1128 <37084688+blackbird1128@users.noreply.github.com>
Date: Fri, 15 Nov 2024 17:35:19 +0100
Subject: [PATCH 2/2] add a note in CHANGES.md

---
 CHANGES.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGES.md b/CHANGES.md
index f8f63f52c..e68594a19 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,7 @@
 # unreleased
 ------------
 
+ - [fcc] fix the output of the AST dump plugin to be valid JSON
  - [fleche] fix quick fixes for errors being lost due to incorrect
    handling of `send_diags_extra_data` (@ejgallego, #850)
  - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)