diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 11 |
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 |