From e9a3f2edd58a4deb85a0342c79e52d530dd2a50b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 23 Oct 2024 15:16:41 +0200
Subject: [PATCH] Adapt to coq/coq#19741 (parse_extra has an additionnal
 argument)

---
 language-server/dm/delegationManager.ml  | 4 ++--
 language-server/dm/delegationManager.mli | 2 +-
 language-server/dm/executionManager.mli  | 2 +-
 language-server/dm/parTactic.mli         | 2 +-
 language-server/vscoqtop/vscoqtop.ml     | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/language-server/dm/delegationManager.ml b/language-server/dm/delegationManager.ml
index ebe9f868..38f1ab88 100644
--- a/language-server/dm/delegationManager.ml
+++ b/language-server/dm/delegationManager.ml
@@ -96,7 +96,7 @@ module type Worker = sig
   
   (* for worker toplevels *)
   type options
-  val parse_options : string list -> options * string list
+  val parse_options : Coqargs.t -> string list -> options * string list
   (* the sentence ids of the remote_mapping being delegated *)
   val setup_plumbing : options -> ((job_update_request -> unit) * job_t)
   
@@ -331,7 +331,7 @@ let setup_plumbing port =
     log_worker @@ Printf.sprintf "error starting: %s: %s: %s" syscall param (Unix.error_message code);
     exit 1
 
-let parse_options extra_args =
+let parse_options _baseopts extra_args =
   match extra_args with
   | [ o ; port ] when o = option_name -> int_of_string port, []
   | _ ->
diff --git a/language-server/dm/delegationManager.mli b/language-server/dm/delegationManager.mli
index 9b0856bb..014f348e 100644
--- a/language-server/dm/delegationManager.mli
+++ b/language-server/dm/delegationManager.mli
@@ -79,7 +79,7 @@ module type Worker = sig
    
    (* for worker toplevels *)
    type options
-   val parse_options : string list -> options * string list
+   val parse_options : Coqargs.t -> string list -> options * string list
    (* the sentence ids of the remote_mapping being delegated *)
    val setup_plumbing : options -> ((job_update_request -> unit) * job_t)
    
diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli
index f2ff71c8..f6f6ed2e 100644
--- a/language-server/dm/executionManager.mli
+++ b/language-server/dm/executionManager.mli
@@ -87,7 +87,7 @@ val print_exec_overview_of_state : state -> unit
 (** Coq toplevels for delegation without fork *)
 module ProofWorkerProcess : sig
   type options
-  val parse_options : string list -> options * string list
+  val parse_options : Coqargs.t -> string list -> options * string list
   val main : st:Vernacstate.t -> options -> unit
   val log : string -> unit
 end
diff --git a/language-server/dm/parTactic.mli b/language-server/dm/parTactic.mli
index 3df34d22..57e8ad1e 100644
--- a/language-server/dm/parTactic.mli
+++ b/language-server/dm/parTactic.mli
@@ -13,7 +13,7 @@
 (**************************************************************************)
 module TacticWorkerProcess : sig
   type options
-  val parse_options : string list -> options * string list
+  val parse_options : Coqargs.t -> string list -> options * string list
   val main : st:Vernacstate.t -> options -> unit
   val log : string -> unit
 end
diff --git a/language-server/vscoqtop/vscoqtop.ml b/language-server/vscoqtop/vscoqtop.ml
index 4c525888..d7608b87 100644
--- a/language-server/vscoqtop/vscoqtop.ml
+++ b/language-server/vscoqtop/vscoqtop.ml
@@ -70,7 +70,7 @@ let _ =
       let args = CoqProject_file.coqtop_args_from_project project in
       log (Printf.sprintf "Arguments from project file %s: %s" f (String.concat " " args));
       fst @@ Coqargs.parse_args ~usage:vscoqtop_specific_usage ~init:Coqargs.default args in
-  let opts, () = Coqinit.parse_arguments ~usage:vscoqtop_specific_usage ~initial_args ~parse_extra:(fun x -> skip_xd [] x) () in
+  let opts, () = Coqinit.parse_arguments ~usage:vscoqtop_specific_usage ~initial_args ~parse_extra:(fun _ x -> skip_xd [] x) () in
   let injections = Coqinit.init_runtime opts in
   Safe_typing.allow_delayed_constants := true; (* Needed to delegate or skip proofs *)
   Sys.(set_signal sigint Signal_ignore);