aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts/coqmktop.ml
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-05-23 15:13:07 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-05-23 15:13:07 +0000
commitdc2e676c9cdedea43805c21a4b3203832a985f95 (patch)
tree849760ef13d1460d603ce9436c244922e13a6080 /scripts/coqmktop.ml
parenta023ff2e48aaf7ebfb15e10dc7cdb80ab2991e8e (diff)
amelioration des messages d'erreurs vis a vis des evars
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts/coqmktop.ml')
-rw-r--r--scripts/coqmktop.ml11
1 files changed, 5 insertions, 6 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index ee3acb5f4..8e80e6dcb 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -238,9 +238,11 @@ let declare_loading_string () =
"Mltop.set Mltop.WithoutTop;;\n"
else
"let ppf = Format.std_formatter;;
- Mltop.set (Mltop.WithTop {Mltop.load_obj=Topdirs.dir_load ppf;
- Mltop.use_file=Topdirs.dir_use ppf;
- Mltop.add_dir=Topdirs.dir_directory});;\n"
+ Mltop.set (Mltop.WithTop
+ {Mltop.load_obj=Topdirs.dir_load ppf;
+ Mltop.use_file=Topdirs.dir_use ppf;
+ Mltop.add_dir=Topdirs.dir_directory;
+ Mltop.ml_loop=(fun () -> Toploop.loop ppf) });;\n"
(* create a temporary main file to link *)
let create_tmp_main_file modules =
@@ -258,9 +260,6 @@ let create_tmp_main_file modules =
output_string oc "Cmd_searchisos_line.start();;\n"
else
output_string oc "Coqtop.start();;\n";
- (* Start the Ocaml toplevel if it exists *)
- if !top then
- output_string oc "Printexc.catch Toploop.loop ppf; exit 1;;\n";
close_out oc;
main_name
with e ->