diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-27 20:16:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-12 16:49:45 +0200 |
| commit | ce2b2058587224ade9261cd4127ef4f6e94d356b (patch) | |
| tree | 28e9cc9f14c0bb3a8107e67faa85ccda6c6d4dc9 /toplevel/coqinit.ml | |
| parent | 4ed9c7ad75a7f09d723bdfce6f7dd086c60e0601 (diff) | |
[stm] Port the toplevel to the STM.
- We clean-up `Vernac` and make it use the STM API.
- Now functions in `Vernac` for use in the toplevel and compiler take
an starting `Stateid.t`.
- Duplicated `Stm.interp` entry point is removed.
- The XML protocol call `interp` is disabled.
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ffd0d7805..2b9a04dad 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true let load_rc = ref true let no_load_rc () = load_rc := false -let load_rcfile() = +let load_rcfile sid = if !load_rc then try if !rcfile_specified then if CUnix.file_readable_p !rcfile then - Vernac.load_vernac false !rcfile + Vernac.load_vernac false sid !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else try @@ -43,8 +43,8 @@ let load_rcfile() = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac false inferedrc - with Not_found -> () + Vernac.load_vernac false sid inferedrc + with Not_found -> sid (* Flags.if_verbose mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ @@ -55,7 +55,8 @@ let load_rcfile() = let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise else - Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.") + (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = |