this works recovers, but does not admit the failed proof

toplevel/vernac.ml

@@ -57,7 +57,7 @@ module State = struct
     sid : Stateid.t;
     proof : Proof.t option;
     time : time_output option;
-    failed_proofs : Names.Id.t list;
+    failed_proofs : (Names.Id.t * Pp.t) list;
     in_recovery : bool;
     recovery_mode : bool;
   }
@@ -73,59 +73,50 @@ let emit_time state com tstart tend =
     | ToFeedback -> Feedback.msg_notice pp
     | ToChannel ch -> Pp.pp_with ch (pp ++ fnl())
 
+
+let admitted_com =
+  CAst.make { control = []; attrs = []; expr =
+    (VernacSynPure (VernacEndProof Admitted))}
+
 let interp_vernac ~check ~state ({CAst.loc;_} as com) =
   let open State in
 
-    let current_proof_name =
-      match state.proof with 
-        Some prf -> Some ((Proof.data prf).name)
-      | None -> None in
-
-    let admitted_com =
-      CAst.make { control = []; attrs = []; expr =
-        (VernacSynPure (VernacEndProof Admitted))}in
     try
 
-      let new_recovery_status, the_com =
-        if state.in_recovery then 
+      let new_recovery_status, com =
+        if state.in_recovery then
           (match Vernac_classifier.classify_vernac com with
-            Vernacextend.VtQed _ -> false, Some admitted_com
-            | _ -> true, None)
-          else false, Some com in
+            Vernacextend.VtQed _ -> false, admitted_com
+            | _ -> true, com)
+          else false, com in
 
-      let doc, nsid, ntip = 
-        match the_com with 
-        | Some com ->
-          Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com
-        | None -> state.doc, state.sid, Stm.NewAddTip in
+      let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in
 
       (* Main STM interaction *)
       if ntip <> Stm.NewAddTip then
         anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
-
-
+
       (* Force the command  *)
-      let () = if check && not state.in_recovery then Stm.observe ~doc nsid in
-      let new_proof = Vernacstate.Declare.give_me_the_proof_opt () [@ocaml.warning "-3"] in
-      { state with doc; sid = nsid; proof = new_proof;
-        in_recovery = new_recovery_status}
-    with potentially_catched ->
-      let (reraise, info) = Exninfo.capture potentially_catched in
+      try 
+        let () = if check && not state.in_recovery then Stm.observe ~doc nsid in
+        let new_proof = Vernacstate.Declare.give_me_the_proof_opt () [@ocaml.warning "-3"] in
+        { state with doc; sid = nsid; proof = new_proof;
+          in_recovery = new_recovery_status}
+      with potentially_catched when noncritical potentially_catched ->
+        match state.proof with
+        | Some prf ->
+          {state with doc; sid = nsid; in_recovery = true;
+          failed_proofs = ((Proof.data prf).name, print potentially_catched) ::
+            state.failed_proofs}
+        | None -> raise potentially_catched
+    with reraise ->
+      let (reraise, info) = Exninfo.capture reraise in
       let info =
         (* Set the loc to the whole command if no loc *)
         match Loc.get_loc info, loc with
         | None, Some loc -> Loc.add_loc info loc
-        | Some _, _ | _, None  -> info in
-      if state.recovery_mode then
-        match current_proof_name with
-          Some proof_name ->
-            if CErrors.noncritical potentially_catched then
-              {state with in_recovery = true;
-                failed_proofs = proof_name :: state.failed_proofs}
-            else
-              Exninfo.iraise (reraise, info)
-          | None -> Exninfo.iraise (reraise, info)
-      else Exninfo.iraise (reraise, info)
+        | Some _, _ | _, None  -> info
+       in Exninfo.iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
 let load_vernac_core ~echo ~check ~state ?source file =
@@ -259,11 +250,13 @@ let beautify_pass ~doc ~comments ~ids ~filename =
    pass. *)
 let load_vernac ~echo ~check ~state ?source filename =
   let ostate, ids, comments = load_vernac_core ~echo ~check ~state ?source filename in
-    if 1 <= List.length (ostate.failed_proofs) then
-      user_err (Pp.str "proofs failed in this file "
+    if 1 <= List.length ostate.failed_proofs then
+      user_err (Pp.str "proofs failed in this file" ++ fnl()
       ++ (ostate.failed_proofs
                         |> List.rev
-                        |> prlist_with_sep pr_comma Names.Id.print)
+                        |> prlist_with_sep fnl
+                          (fun (x, y) -> Names.Id.print x ++ Pp.fnl() ++
+                            y))
                     ++ str ".");
   (* Pass for beautify *)
   if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:(List.rev ids) ~filename;

toplevel/vernac.mli

@@ -20,7 +20,7 @@ module State : sig
     sid : Stateid.t;
     proof : Proof.t option;
     time : time_output option;
-    failed_proofs : Names.Id.t list;
+    failed_proofs : (Names.Id.t * Pp.t) list;
     in_recovery : bool;
     recovery_mode : bool
   }