summaryrefslogtreecommitdiff
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml11
1 files changed, 8 insertions, 3 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 76e9c2fe..a60e0d82 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -247,10 +247,13 @@ let parse_args arglist =
| "-compat" :: [] -> usage ()
| "-vm" :: rem -> use_vm := true; parse rem
- | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
+ | "-emacs" :: rem ->
+ Flags.print_emacs := true; Pp.make_pp_emacs();
+ Vernacentries.qed_display_script := false;
+ parse rem
| "-emacs-U" :: rem ->
warning "Obsolete option \"-emacs-U\", use -emacs instead.";
- Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
+ parse ("-emacs" :: rem)
| "-unicode" :: rem -> add_require "Utf8_core"; parse rem
@@ -326,6 +329,7 @@ let init arglist =
if_verbose print_header ();
init_load_path ();
inputstate ();
+ Mltop.init_known_plugins ();
set_vm_opt ();
engage ();
if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
@@ -349,7 +353,8 @@ let init arglist =
Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
Profile.print_profile ();
exit 0);
- Lib.declare_initial_state ()
+ (* We initialize the command history stack with a first entry *)
+ Backtrack.mark_command Vernacexpr.VernacNop
let init_toplevel = init