diff options
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 3 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 10 |
4 files changed, 6 insertions, 9 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 5d8cdc30fd..2bc217fa35 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 5dba938b5e..98f0acb957 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 f985cfe207..407c1ed1c7 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 de2a81b7c9..b27f7ae31a 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 |