Undo: if the ui is coqtop (command line) then Undo is not part of the doc.

4 files changed, 6 insertions, 9 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 5d8cdc30f..2bc217fa3 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -75,6 +75,7 @@ let debug = ref false
 let profile = false
 
 let print_emacs = ref false
+let coqtop_ui = ref false
 
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
diff --git a/lib/flags.mli b/lib/flags.mli
index 5dba938b5..98f0acb95 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -36,6 +36,7 @@ val debug : bool ref
 val profile : bool
 
 val print_emacs : bool ref
+val coqtop_ui : bool ref
 
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
diff --git a/stm/stm.ml b/stm/stm.ml
index f985cfe20..407c1ed1c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1466,7 +1466,8 @@ end = struct
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun n (id,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          VtStm (VtBack oid, true), VtLater
+          if n = 1 && !Flags.coqtop_ui then VtStm (VtBack oid, false), VtNow
+          else VtStm (VtBack oid, true), VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
           let m = match e with VernacUndoTo m -> m | _ -> 0 in
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index de2a81b7c..b27f7ae31 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -339,14 +339,8 @@ let feed_emacs = function
 
 let rec loop () =
   Sys.catch_break true;
-  if !Flags.print_emacs then begin
-    (* TODO : check with Enrico ?! *)
-    (*
-    Pp.set_feeder feed_emacs;
-    Vernacentries.enable_goal_printing := false;
-    *)
-    Vernacentries.qed_display_script := false;
-  end;
+  if !Flags.print_emacs then Vernacentries.qed_display_script := false;
+  Flags.coqtop_ui := true;
   try
     reset_input_buffer stdin top_buffer;
     while true do do_vernac(); flush_all() done