diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
| commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
| tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /toplevel/coqtop.ml | |
| parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) | |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
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 |