aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqloop.ml63
-rw-r--r--toplevel/coqloop.mli2
-rw-r--r--toplevel/coqtop.ml28
-rw-r--r--toplevel/vernac.ml9
4 files changed, 68 insertions, 34 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 2cb6083261..e9506803df 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -14,8 +14,7 @@ open Vernac
open Pcoq
let top_stderr x =
- pp_with ~pp_tag:Ppstyle.to_format !Pp_control.err_ft x;
- Format.pp_print_flush !Pp_control.err_ft ()
+ Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ~pp_tag:Ppstyle.to_format) x
(* A buffer for the character read from a channel. We store the command
* entered to be able to report errors without pretty-printing. *)
@@ -253,7 +252,8 @@ let print_toplevel_error (e, info) =
else mt ()
else print_location_in_file loc
in
- locmsg ++ CErrors.iprint (e, info)
+ let hdr msg = hov 0 (tag Ppstyle.error_tag (str "Error:") ++ spc () ++ msg) in
+ locmsg ++ hdr (CErrors.iprint (e, info))
(* Read the input stream until a dot is encountered *)
let parse_to_dot =
@@ -285,6 +285,33 @@ let read_sentence input =
discard_to_dot ();
iraise reraise
+(** Coqloop Console feedback handler *)
+let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
+ match fb.contents with
+ | Processed -> ()
+ | Incomplete -> ()
+ | Complete -> ()
+ | ProcessingIn _ -> ()
+ | InProgress _ -> ()
+ | WorkerStatus (_,_) -> ()
+ | AddedAxiom -> ()
+ | GlobRef (_,_,_,_,_) -> ()
+ | GlobDef (_,_,_,_) -> ()
+ | FileDependency (_,_) -> ()
+ | FileLoaded (_,_) -> ()
+ | Custom (_,_,_) -> ()
+ | Message (Error,loc,msg) ->
+ (* We ignore errors here as we (still) have a different error
+ printer for the toplevel. It is hard to solve due the many
+ error paths presents, and the different compromise of feedback
+ error forwaring in the stm depending on the mode *)
+ ()
+ | Message (lvl,loc,msg) ->
+ if !Flags.print_emacs then
+ Topfmt.emacs_logger ?loc lvl msg
+ else
+ Topfmt.std_logger ?loc lvl msg
+
(** [do_vernac] reads and executes a toplevel phrase, and print error
messages when an exception is raised, except for the following:
- Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
@@ -307,12 +334,13 @@ let do_vernac () =
top_stderr (fnl ()); raise CErrors.Quit
| CErrors.Drop -> (* Last chance *)
if Mltop.is_ocaml_top() then raise CErrors.Drop
- else Feedback.msg_error (str"There is no ML toplevel.")
+ else top_stderr (str "There is no ML toplevel.")
| any ->
+ (** Main error printer, note that this didn't it the "emacs"
+ legacy path. *)
let any = CErrors.push any in
let msg = print_toplevel_error any ++ fnl () in
- pp_with !Pp_control.std_ft msg;
- Format.pp_print_flush !Pp_control.std_ft ()
+ top_stderr msg
(** Main coq loop : read vernacular expressions until Drop is entered.
Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -320,22 +348,13 @@ let do_vernac () =
exit the loop are Drop and Quit. Any other exception there indicates
an issue with [print_toplevel_error] above. *)
-(*
-let feed_emacs = function
- | { Interface.id = Interface.State id;
- Interface.content = Interface.GlobRef (_,a,_,c,_) } ->
- prerr_endline ("<info>" ^"<id>"^Stateid.to_string id ^"</id>"
- ^a^" "^c^ "</info>")
- | _ -> ()
-*)
-
(* Flush in a compatible order with 8.5 *)
(* This mimics the semantics of the old Pp.flush_all *)
let loop_flush_all () =
Pervasives.flush stderr;
Pervasives.flush stdout;
- Format.pp_print_flush !Pp_control.std_ft ();
- Format.pp_print_flush !Pp_control.err_ft ()
+ Format.pp_print_flush !Topfmt.std_ft ();
+ Format.pp_print_flush !Topfmt.err_ft ()
let rec loop () =
Sys.catch_break true;
@@ -348,9 +367,9 @@ let rec loop () =
| CErrors.Drop -> ()
| CErrors.Quit -> exit 0
| any ->
- Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
- str (Printexc.to_string any) ++
- fnl() ++
- str"Please report" ++
- strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
+ top_stderr (str"Anomaly: main loop exited with exception: " ++
+ str (Printexc.to_string any) ++
+ fnl() ++
+ str"Please report" ++
+ strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
loop ()
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index d248f2f706..eb61084e09 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -32,6 +32,8 @@ val set_prompt : (unit -> string) -> unit
val print_toplevel_error : Exninfo.iexn -> std_ppcmds
+val coqloop_feed : Feedback.feedback -> unit
+
(** Parse and execute one vernac command. *)
val do_vernac : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 541c1fd1bb..823d05580b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -61,7 +61,7 @@ let init_color () =
match colors with
| None ->
(** Default colors *)
- Feedback.init_color_output ()
+ Topfmt.init_color_output ()
| Some "" ->
(** No color output *)
()
@@ -69,7 +69,7 @@ let init_color () =
(** Overwrite all colors *)
Ppstyle.clear_styles ();
Ppstyle.parse_config s;
- Feedback.init_color_output ()
+ Topfmt.init_color_output ()
end
let toploop_init = ref begin fun x ->
@@ -78,15 +78,27 @@ let toploop_init = ref begin fun x ->
x
end
-let toploop_run = ref (fun () ->
+(* Feedback received in the init stage, this is different as the STM
+ will not be generally be initialized, thus stateid, etc... may be
+ bogus. For now we just print to the console too *)
+let coqtop_init_feed = Coqloop.coqloop_feed
+
+(* Default toplevel loop *)
+let console_toploop_run () =
+ (* We initialize the console only if we run the toploop_run *)
+ let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
if Dumpglob.dump () then begin
if_verbose warning "Dumpglob cannot be used in interactive mode.";
Dumpglob.noglob ()
end;
Coqloop.loop();
+ (* We remove the feeder but it could be ok not to do so *)
+ Feedback.del_feeder tl_feed;
(* Initialise and launch the Ocaml toplevel *)
Coqinit.init_ocaml_path();
- Mltop.ocaml_toploop())
+ Mltop.ocaml_toploop()
+
+let toploop_run = ref console_toploop_run
let output_context = ref false
@@ -228,7 +240,6 @@ let compile_files () =
if !compile_list == [] then ()
else
let init_state = States.freeze ~marshallable:`No in
- Feedback.(add_feeder debug_feeder);
List.iter (fun vf ->
States.unfreeze init_state;
compile_file vf)
@@ -240,7 +251,6 @@ let set_emacs () =
if not (Option.is_empty !toploop) then
error "Flag -emacs is incompatible with a custom toplevel loop";
Flags.print_emacs := true;
- Feedback.(set_logger emacs_logger);
Vernacentries.qed_display_script := false;
color := `OFF
@@ -435,7 +445,7 @@ let get_native_name s =
with the appropriate error code *)
let fatal_error info anomaly =
let msg = info ++ fnl () in
- Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg;
+ Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ?pp_tag:None) msg;
exit (if anomaly then 129 else 1)
let parse_args arglist =
@@ -609,6 +619,7 @@ let parse_args arglist =
let init_toplevel arglist =
init_gc ();
Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
+ let init_feeder = Feedback.add_feeder coqtop_init_feed in
Lib.init();
begin
try
@@ -663,7 +674,8 @@ let init_toplevel arglist =
Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
Profile.print_profile ();
exit 0
- end
+ end;
+ Feedback.del_feeder init_feeder
let start () =
let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5d17054fce..4fc4540c1c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -143,8 +143,8 @@ let pr_new_syntax_in_context loc chan_beautify ocom =
| None -> mt() in
let after = comment (CLexer.extract_comments (snd loc)) in
if !beautify_file then
- (Pp.pp_with !Pp_control.std_ft (hov 0 (before ++ com ++ after));
- Format.pp_print_flush !Pp_control.std_ft ())
+ (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after));
+ Format.pp_print_flush !Topfmt.std_ft ())
else
Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
States.unfreeze fs;
@@ -179,9 +179,10 @@ let pp_cmd_header loc com =
(* This is a special case where we assume we are in console batch mode
and take control of the console.
*)
+(* FIXME *)
let print_cmd_header loc com =
- Pp.pp_with ~pp_tag:Ppstyle.to_format !Pp_control.std_ft (pp_cmd_header loc com);
- Format.pp_print_flush !Pp_control.std_ft ()
+ Pp.pp_with ~pp_tag:Ppstyle.to_format !Topfmt.std_ft (pp_cmd_header loc com);
+ Format.pp_print_flush !Topfmt.std_ft ()
let rec interp_vernac po chan_beautify checknav (loc,com) =
let interp = function
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-03 22:26:25 +0000