[coq] Utils.with_control use VernacControl (adapt to coq/coq#19517 ad…

…ding a control flag)

coq/utils.ml

@@ -45,47 +45,16 @@ let to_range ~lines (p : Loc.t) : Lang.Range.t =
 
 let to_orange ~lines = Option.map (to_range ~lines)
 
-(* Separation of parsing and execution made upstream API hard to use for us
-   :/ *)
-let pmeasure (measure, print) fn =
-  match measure fn () with
-  | Ok _ as r -> Feedback.msg_notice @@ print r
-  | Error (exn, _) as r ->
-    Feedback.msg_notice @@ print r;
-    Exninfo.iraise exn
-
-let with_fail fn =
-  try
-    fn ();
-    CErrors.user_err (Pp.str "The command has not failed!")
-  with exn when CErrors.noncritical exn ->
-    let exn = Exninfo.capture exn in
-    let msg = CErrors.iprint exn in
-    Feedback.msg_notice ?loc:None
-      Pp.(str "The command has indeed failed with message:" ++ fnl () ++ msg)
-
-let with_ctrl ctrl ~st ~fn =
-  let st = State.to_coq st in
-  match ctrl with
-  | Vernacexpr.ControlTime ->
-    pmeasure System.(measure_duration, fmt_transaction_result) fn
-  | Vernacexpr.ControlInstructions ->
-    pmeasure System.(count_instructions, fmt_instructions_result) fn
-  | Vernacexpr.ControlTimeout n -> (
-    match Control.timeout (float_of_int n) fn () with
-    | None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout)
-    | Some x -> x)
-  (* fail and succeed *)
-  | Vernacexpr.ControlFail ->
-    with_fail fn;
-    Vernacstate.Interp.invalidate_cache ();
-    Vernacstate.unfreeze_full_state st
-  | Vernacexpr.ControlSucceed ->
-    fn ();
-    Vernacstate.Interp.invalidate_cache ();
-    Vernacstate.unfreeze_full_state st
-  (* Unsupported by coq-lsp, maybe deprecate upstream *)
-  | Vernacexpr.ControlRedirect _ -> fn ()
-
 let with_control ~fn ~control ~st =
-  List.fold_right (fun ctrl fn () -> with_ctrl ctrl ~st ~fn) control fn ()
+  let open VernacControl in
+  let control = from_syntax control in
+  let control, () =
+    under_control ~loc:None ~with_local_state:trivial_state control ~noop:() fn
+  in
+  let noop = after_last_phase ~loc:None control in
+  let () =
+    if noop then (
+      Vernacstate.Interp.invalidate_cache ();
+      Vernacstate.unfreeze_full_state (State.to_coq st))
+  in
+  ()