aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml6
-rw-r--r--toplevel/coqtop_bin.ml2
-rw-r--r--toplevel/coqtop_byte_bin.ml21
-rw-r--r--toplevel/coqtop_opt_bin.ml3
4 files changed, 28 insertions, 4 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6048dae3b..2fa9f0ab4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -756,7 +756,7 @@ let init_toplevel arglist =
(* Coq's init process, phase 1:
- OCaml parameters, and basic structures and IO
*)
- Profile.init_profile ();
+ CProfile.init_profile ();
init_gc ();
Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
let init_feeder = Feedback.add_feeder coqtop_init_feed in
@@ -846,7 +846,5 @@ let start () =
let sigma, env = Pfedit.get_current_context () in
Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
end;
- Profile.print_profile ();
+ CProfile.print_profile ();
exit 0
-
-(* [Coqtop.start] will be called by the code produced by coqmktop *)
diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml
new file mode 100644
index 000000000..56aced92a
--- /dev/null
+++ b/toplevel/coqtop_bin.ml
@@ -0,0 +1,2 @@
+(* Main coqtop initialization *)
+let () = Coqtop.start()
diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml
new file mode 100644
index 000000000..7d8354ec3
--- /dev/null
+++ b/toplevel/coqtop_byte_bin.ml
@@ -0,0 +1,21 @@
+let drop_setup () =
+ begin try
+ (* Enable rectypes in the toplevel if it has the directive #rectypes *)
+ begin match Hashtbl.find Toploop.directive_table "rectypes" with
+ | Toploop.Directive_none f -> f ()
+ | _ -> ()
+ end
+ with
+ | Not_found -> ()
+ end;
+ let ppf = Format.std_formatter in
+ Mltop.(set_top
+ { load_obj = (fun f -> if not (Topdirs.load_file ppf f)
+ then CErrors.user_err Pp.(str ("Could not load plugin "^f))
+ );
+ use_file = Topdirs.dir_use ppf;
+ add_dir = Topdirs.dir_directory;
+ ml_loop = (fun () -> Toploop.loop ppf);
+ })
+
+let _ = drop_setup ()
diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml
new file mode 100644
index 000000000..410b4679a
--- /dev/null
+++ b/toplevel/coqtop_opt_bin.ml
@@ -0,0 +1,3 @@
+let drop_setup () = Mltop.remove ()
+
+let _ = drop_setup ()