diff options
| author | monate | 2003-02-04 16:45:50 +0000 |
|---|---|---|
| committer | monate | 2003-02-04 16:45:50 +0000 |
| commit | 3fe1d8e42877e07e744911fcd2b5a9c7afe988f6 (patch) | |
| tree | 7a3fc7da6f7f8880ee693dc00ada57c4ab980e05 /toplevel | |
| parent | 341eb14c1e5770eab5c12cbf5e38d7d6b4fa3599 (diff) | |
interface GTK2 experimentale
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3660 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 10 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 7 |
2 files changed, 13 insertions, 4 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6c56ca10bd..c136507fb1 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -215,11 +215,10 @@ let parse_args () = (* To prevent from doing the initialization twice *) let initialized = ref false -(* Ctrl-C is fatal during the initialisation *) -let start () = +let init () = if not !initialized then begin initialized := true; - Sys.catch_break false; + Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) Lib.init(); try parse_args (); @@ -241,7 +240,10 @@ let start () = exit 1 end; if !batch_mode then (flush_all(); Profile.print_profile (); exit 0); - Lib.declare_initial_state (); + Lib.declare_initial_state () + +let start () = + init (); Toplevel.loop(); (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index ff4e169d9e..42618505f7 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -14,3 +14,10 @@ produce the output state if any, and finally will launch [Toplevel.loop]. *) val start : unit -> unit + +(* [init] is already called by [start], but exported here to be reused + by the Coq IDE. It does everything [start] does, except launching + the toplevel loop. *) + +val init : unit -> unit + |