Merge pull request #774 from ejgallego/support_abort_all

[fleche] Support `Abort All`.

CHANGES.md

@@ -49,6 +49,8 @@
    (@ejgallego, Diego Rivera, #772)
  - [hover] New option `show_universes_on_hover` that will display
    universe data on hover (@ejgallego, @SkySkimmer, #666)
+ - [fleche] Support meta-command `Abort All` (@ejgallego, #, fixes
+   #550)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

coq/ast.ml

@@ -77,6 +77,9 @@ module Meta = struct
       | Back of int
       | ResetName of Names.lident
       | ResetInitial
+      | AbortAll
+    (* Not supported, but actually easy if we want | VernacRestart | VernacUndo
+       _ | VernacUndoTo _ *)
     [@@deriving hash, compare]
   end
 
@@ -104,6 +107,9 @@ module Meta = struct
       | { expr = VernacSynPure (VernacBack num); control; attrs } ->
         let command = Command.Back num in
         Some { command; loc; attrs; control }
+      | { expr = VernacSynPure VernacAbortAll; control; attrs } ->
+        let command = Command.AbortAll in
+        Some { command; loc; attrs; control }
       | _ -> None)
 end
 

coq/ast.mli

@@ -40,6 +40,7 @@ module Meta : sig
       | Back of int
       | ResetName of Names.lident
       | ResetInitial
+      | AbortAll
   end
 
   type t =

coq/state.ml

@@ -87,7 +87,7 @@ let lemmas ~st = st.Vernacstate.interp.lemmas
 let program ~st =
   NeList.head st.Vernacstate.interp.program |> Declare.OblState.view
 
-let drop_proofs ~st =
+let drop_proof ~st =
   let open Vernacstate in
   let interp =
     { st.interp with
@@ -99,6 +99,11 @@ let drop_proofs ~st =
   in
   { st with interp }
 
+let drop_all_proofs ~st =
+  let open Vernacstate in
+  let interp = { st.interp with lemmas = None } in
+  { st with interp }
+
 let in_state ~token ~st ~f a =
   let f a =
     Vernacstate.unfreeze_full_state st;

coq/state.mli

@@ -29,8 +29,11 @@ val in_stateM :
   -> 'a
   -> ('b, Loc.t) Protect.E.t
 
-(** Drop the proofs from the state *)
-val drop_proofs : st:t -> t
+(** Drop the top proof from the state *)
+val drop_proof : st:t -> t
+
+(** Drop all proofs from the state *)
+val drop_all_proofs : st:t -> t
 
 (** Fully admit an ongoing proof *)
 val admit : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t

examples/MetaCommands.v

@@ -34,5 +34,13 @@ About muu.
 About foo.
 About bar.
 
+Lemma foo : True.
+  Lemma bar : False.
+  Abort All.
+
+Lemma foo : True. now auto. Qed.
+
+Print foo.
+
 
 

fleche/doc.ml

@@ -660,7 +660,7 @@ let interp_and_info ~token ~st ~files ast =
   | Some ast -> Memo.Require.evalS ~token (st, files, ast)
 
 (* Support for meta-commands, a bit messy, but cool in itself *)
-let search_node ~command ~doc =
+let search_node ~command ~doc ~st =
   let nstats (node : Node.t option) =
     Option.cata
       (fun (node : Node.t) -> Option.default Memo.Stats.zero node.info.stats)
@@ -689,6 +689,9 @@ let search_node ~command ~doc =
       let node = Option.default node node.prev in
       (Coq.Protect.E.ok node.state, nstats (Some node)))
   | ResetInitial -> (Coq.Protect.E.ok doc.root, nstats None)
+  | AbortAll ->
+    let st = Coq.State.drop_all_proofs ~st in
+    (Coq.Protect.E.ok st, nstats None)
 
 let interp_and_info ~token ~st ~files ~doc ast =
   match Coq.Ast.Meta.extract ast with
@@ -698,7 +701,7 @@ let interp_and_info ~token ~st ~files ~doc ast =
        spending on error recovery and meta stuff, we should record that time
        actually at some point too. In this case, maybe we could recover the
        cache hit from the original node? *)
-    search_node ~command ~doc
+    search_node ~command ~doc ~st
 
 let interp_and_info ~token ~parsing_time ~st ~files ~doc ast =
   let res, stats = interp_and_info ~token ~st ~files ~doc ast in