[petanque] Allow init to be called multiple times

We need to rework the protocol as to better reflect the Coq/Flèche
workspace mode, but this hotfix will work meanwhile.

CHANGES.md

@@ -32,6 +32,8 @@
  - [code] Don't start server on extension activation, unless an editor
    we own is active. We also auto-start the server if a document that
    we own is opened later (@ejgallego, #758, fixes #750)
+ - [petanque] Allow `init` to be called multiple times (@ejgallego,
+   @gbdrt, #766)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

petanque/agent.ml

@@ -118,16 +118,28 @@ let print_diags (doc : Fleche.Doc.t) =
   let d = Fleche.Doc.diags doc in
   Format.(eprintf "@[<v>%a@]" (pp_print_list pp_diag) d)
 
-let init ~token ~debug ~root =
-  let init = init_coq ~debug in
-  Fleche.Io.CallBack.set io;
+let setup_workspace ~token ~init ~debug ~root =
   let dir = Lang.LUri.File.to_string_file root in
   (let open Coq.Compat.Result.O in
    let+ workspace = Coq.Workspace.guess ~token ~debug ~cmdline ~dir in
    let files = Coq.Files.make () in
    Fleche.Doc.Env.make ~init ~workspace ~files)
   |> Result.map_error (fun msg -> Error.Coq msg)
 
+let init_st = ref None
+
+let init ~token ~debug ~root =
+  let init =
+    match !init_st with
+    | None ->
+      let init = init_coq ~debug in
+      Fleche.Io.CallBack.set io;
+      init_st := Some init;
+      init
+    | Some init -> init
+  in
+  setup_workspace ~token ~init ~debug ~root
+
 let start ~token ~env ~uri ~thm =
   match read_raw ~uri with
   | Ok raw ->

petanque/test/basic_api.ml

@@ -23,6 +23,8 @@ let start ~token =
   (* Will this work on Windows? *)
   let open Coq.Compat.Result.O in
   let root, uri = prepare_paths () in
+  (* Twice to test for #766 *)
+  let* _env = Agent.init ~token ~debug ~root in
   let* env = Agent.init ~token ~debug ~root in
   Agent.start ~token ~env ~uri ~thm:"rev_snoc_cons"