diff options
| -rw-r--r-- | toplevel/coqloop.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 10 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 5 |
4 files changed, 17 insertions, 7 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 9a4f476bd..a80599cd5 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -173,12 +173,13 @@ let print_error_for_buffer ?loc lvl msg buf = then Topfmt.emacs_logger ?pre_hdr lvl msg else Topfmt.std_logger ?pre_hdr lvl msg +(* let print_toplevel_parse_error (e, info) buf = let loc = Loc.get_loc info in let lvl = Feedback.Error in let msg = CErrors.iprint (e, info) in print_error_for_buffer ?loc lvl msg buf - +*) end (*s The Coq prompt is the name of the focused proof, if any, and "Coq" @@ -260,7 +261,10 @@ let read_sentence sid input = with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); - TopErr.print_toplevel_parse_error reraise top_buffer; + (* The caller of read_sentence does the error printing now, this + should be re-enabled once we rely on the feedback error + printer again *) + (* TopErr.print_toplevel_parse_error reraise top_buffer; *) Exninfo.iraise reraise (** Coqloop Console feedback handler *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5687418f2..8f50bfb3d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -292,9 +292,17 @@ let init_gc () = We no longer use [Arg.parse], in order to use share [Usage.print_usage] between coqtop and coqc. *) +let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem" + (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") + +exception NoCoqLib let usage () = - Envars.set_coqlib ~fail:CErrors.error; + begin + try + Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib); init_load_path (); + with NoCoqLib -> usage_no_coqlib () + end; if !batch_mode then Usage.print_usage_coqc () else begin Mltop.load_ml_objects_raw_rex diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e457ca61d..e29048035 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -30,6 +30,7 @@ let print_usage_channel co command = \n -R dir coqdir recursively map physical dir to logical coqdir\ \n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ +\n -coqlib dir set the coq standard library directory\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ \n -noinit start without loading the Init library\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9f6f77ef1..4fca4ea18 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -323,8 +323,5 @@ let compile verbosely f = let compile v f = ignore(CoqworkmgrApi.get 1); - begin - try compile v f - with any -> Topfmt.print_err_exn any - end; + compile v f; CoqworkmgrApi.giveback 1 |