aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/class.ml4
-rw-r--r--toplevel/command.ml12
-rw-r--r--toplevel/coqinit.ml10
-rw-r--r--toplevel/coqloop.ml16
-rw-r--r--toplevel/coqtop.ml24
-rw-r--r--toplevel/indschemes.ml4
-rw-r--r--toplevel/locality.ml2
-rw-r--r--toplevel/metasyntax.ml16
-rw-r--r--toplevel/mltop.ml10
-rw-r--r--toplevel/obligations.ml18
-rw-r--r--toplevel/record.ml4
-rw-r--r--toplevel/vernac.ml23
-rw-r--r--toplevel/vernacentries.ml112
-rw-r--r--toplevel/vernacinterp.ml4
14 files changed, 131 insertions, 128 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml
index a9c53b4d4..10e9b30be 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -262,7 +262,7 @@ let add_new_coercion_core coef stre poly source target isid =
in
check_source (Some cls);
if not (uniform_cond (llp-ind) lvs) then
- msg_warning (explain_coercion_error coef NotUniform);
+ Feedback.msg_warning (explain_coercion_error coef NotUniform);
let clt =
try
get_target tg ind
@@ -310,7 +310,7 @@ let add_coercion_hook poly local ref =
in
let () = try_add_new_coercion ref stre poly in
let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
- Flags.if_verbose msg_info msg
+ Flags.if_verbose Feedback.msg_info msg
let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5865fec06..f0f678e08 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -119,7 +119,7 @@ let interp_definition pl bl p red_option c ctypopt =
impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *)
in
if not (try List.for_all chk imps2 with Not_found -> false)
- then msg_warning
+ then Feedback.msg_warning
(strbrk "Implicit arguments declaration relies on type." ++ spc () ++
strbrk "The term declares more implicits than the type here.");
let vars = Univ.LSet.union (Universes.universes_of_constr body)
@@ -140,7 +140,7 @@ let get_locality id = function
| Discharge ->
(** If a Let is defined outside a section, then we consider it as a local definition *)
let msg = pr_id id ++ strbrk " is declared as a local definition" in
- let () = msg_warning msg in
+ let () = Feedback.msg_warning msg in
true
| Local -> true
| Global -> false
@@ -171,7 +171,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
let () = if Pfedit.refining () then
let msg = strbrk "Section definition " ++
pr_id ident ++ strbrk " is not visible from current goals" in
- msg_warning msg
+ Feedback.msg_warning msg
in
gr
| Discharge | Local | Global ->
@@ -217,7 +217,7 @@ match local with
let () = assumption_message ident in
let () =
if is_verbose () && Pfedit.refining () then
- msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
+ Feedback.msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
strbrk " is not visible from current goals")
in
let r = VarRef ident in
@@ -706,7 +706,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
constrimpls)
impls;
let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in
- if_verbose msg_info (minductive_message warn_prim names);
+ if_verbose Feedback.msg_info (minductive_message warn_prim names);
if mie.mind_entry_private == None
then declare_default_schemes mind;
mind
@@ -799,7 +799,7 @@ let check_mutuality env isfix fixl =
let po = partial_order Id.equal preorder in
match List.filter (function (_,Inr _) -> true | _ -> false) po with
| (x,Inr xge)::(y,Inr yge)::rest ->
- msg_warning (non_full_mutual_message x xge y yge isfix rest)
+ Feedback.msg_warning (non_full_mutual_message x xge y yge isfix rest)
| _ -> ()
type structured_fixpoint_expr = {
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b81c8da71..e4975fa31 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -36,7 +36,7 @@ let load_rcfile() =
else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
else
try
- let warn x = msg_warning (str x) in
+ let warn x = Feedback.msg_warning (str x) in
let inferedrc = List.find CUnix.file_readable_p [
Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version;
Envars.xdg_config_home warn / rcdefaultname;
@@ -52,10 +52,10 @@ let load_rcfile() =
*)
with reraise ->
let reraise = Errors.push reraise in
- let () = msg_info (str"Load of rcfile failed.") in
+ let () = Feedback.msg_info (str"Load of rcfile failed.") in
iraise reraise
else
- Flags.if_verbose msg_info (str"Skipping rcfile loading.")
+ Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.")
(* Recursively puts dir in the LoadPath if -nois was not passed *)
let add_stdlib_path ~unix_path ~coq_root ~with_ml =
@@ -78,7 +78,7 @@ let push_ml_include s = ml_includes := s :: !ml_includes
let init_load_path () =
let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
- let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in
+ let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
let coqpath = Envars.coqpath in
let coq_root = Names.DirPath.make [Nameops.coq_root] in
(* NOTE: These directories are searched from last to first *)
@@ -135,6 +135,6 @@ let get_compat_version = function
| "8.3" -> Flags.V8_3
| "8.2" -> Flags.V8_2
| ("8.1" | "8.0") as s ->
- msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
+ Feedback.msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
Flags.V8_2
| s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 040c33924..c8879963e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -13,6 +13,8 @@ open Flags
open Vernac
open Pcoq
+let top_stderr x = msg_with !Pp_control.err_ft x
+
(* A buffer for the character read from a channel. We store the command
* entered to be able to report errors without pretty-printing. *)
@@ -59,7 +61,7 @@ let prompt_char ic ibuf count =
| ll::_ -> Int.equal ibuf.len ll
| [] -> Int.equal ibuf.len 0
in
- if bol && not !print_emacs then msgerr (str (ibuf.prompt()));
+ if bol && not !print_emacs then top_stderr (str (ibuf.prompt()));
try
let c = input_char ic in
if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
@@ -310,23 +312,23 @@ let read_sentence () =
*)
let do_vernac () =
- msgerrnl (mt ());
- if !print_emacs then msgerr (str (top_buffer.prompt()));
+ top_stderr (fnl());
+ if !print_emacs then top_stderr (str (top_buffer.prompt()));
resynch_buffer top_buffer;
try
Vernac.eval_expr (read_sentence ())
with
| End_of_input | Errors.Quit ->
- msgerrnl (mt ()); pp_flush(); raise Errors.Quit
+ top_stderr (fnl ()); raise Errors.Quit
| Errors.Drop -> (* Last chance *)
if Mltop.is_ocaml_top() then raise Errors.Drop
- else ppnl (str"Error: There is no ML toplevel." ++ fnl ())
+ else Feedback.msg_error (str"There is no ML toplevel.")
| any ->
let any = Errors.push any in
Format.set_formatter_out_channel stdout;
let msg = print_toplevel_error any ++ fnl () in
pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
- pp_flush ()
+ flush_all ()
(** Main coq loop : read vernacular expressions until Drop is entered.
Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -354,7 +356,7 @@ let rec loop () =
| Errors.Drop -> ()
| Errors.Quit -> exit 0
| any ->
- msgerrnl (str"Anomaly: main loop exited with exception: " ++
+ Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
str (Printexc.to_string any) ++
fnl() ++ str"Please report.");
loop ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c4222b330..869f6bb93 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -31,10 +31,10 @@ let get_version_date () =
let print_header () =
let (ver,rev) = get_version_date () in
- ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
- pp_flush ()
+ Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
+ flush_all ()
-let warning s = with_option Flags.warn msg_warning (strbrk s)
+let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s)
let toploop = ref None
@@ -61,7 +61,8 @@ let init_color () =
match colors with
| None ->
(** Default colors *)
- Ppstyle.init_color_output ()
+ Ppstyle.init_color_output ();
+ Feedback.set_logger Feedback.color_terminal_logger
| Some "" ->
(** No color output *)
()
@@ -69,7 +70,8 @@ let init_color () =
(** Overwrite all colors *)
Ppstyle.clear_styles ();
Ppstyle.parse_config s;
- Ppstyle.init_color_output ()
+ Ppstyle.init_color_output ();
+ Feedback.set_logger Feedback.color_terminal_logger
end
let toploop_init = ref begin fun x ->
@@ -95,8 +97,8 @@ let memory_stat = ref false
let print_memory_stat () =
begin (* -m|--memory from the command-line *)
if !memory_stat then
- ppnl
- (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes");
+ Feedback.msg_notice
+ (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ());
end;
begin
(* operf-macro interface:
@@ -141,7 +143,7 @@ let remove_top_ml () = Mltop.remove ()
let inputstate = ref ""
let set_inputstate s =
- let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in
+ let () = Feedback.msg_warning (str "The inputstate option is deprecated and discouraged.") in
inputstate:=s
let inputstate () =
if not (String.is_empty !inputstate) then
@@ -150,7 +152,7 @@ let inputstate () =
let outputstate = ref ""
let set_outputstate s =
- let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in
+ let () = Feedback.msg_warning (str "The outputstate option is deprecated and discouraged.") in
outputstate:=s
let outputstate () =
if not (String.is_empty !outputstate) then
@@ -243,7 +245,7 @@ let set_emacs () =
if not (Option.is_empty !toploop) then
error "Flag -emacs is incompatible with a custom toplevel loop";
Flags.print_emacs := true;
- Pp.make_pp_emacs ();
+ Feedback.(set_logger emacs_logger);
Vernacentries.qed_display_script := false;
color := `OFF
@@ -646,7 +648,7 @@ let init_toplevel arglist =
if !batch_mode then begin
flush_all();
if !output_context then
- Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
+ Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
Profile.print_profile ();
exit 0
end
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 367425546..f995a390c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -150,7 +150,7 @@ let alarm what internal msg =
| UserAutomaticRequest
| InternalTacticRequest ->
(if debug then
- msg_warning
+ Feedback.msg_warning
(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
| _ -> Some msg
@@ -303,7 +303,7 @@ let declare_congr_scheme ind =
then
ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
else
- msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
+ Feedback.msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
end
let declare_sym_scheme ind =
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index ef789aa5c..c4c891b89 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -35,7 +35,7 @@ let enforce_locality_full locality_flag local =
Errors.error "Use only prefix \"Local\"."
| None ->
if local then begin
- Pp.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix.");
+ Feedback.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix.");
Some true
end else
None
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d60c73939..52117f13f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -568,7 +568,7 @@ let is_not_small_constr = function
let rec define_keywords_aux = function
| GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
when is_not_small_constr e ->
- Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
+ Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
CLexer.add_keyword k;
n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| n :: l -> n :: define_keywords_aux l
@@ -577,7 +577,7 @@ let rec define_keywords_aux = function
(* Ensure that IDENT articulation terminal symbols are keywords *)
let define_keywords = function
| GramConstrTerminal(IDENT k)::l ->
- Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
+ Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
CLexer.add_keyword k;
GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| l -> define_keywords_aux l
@@ -855,12 +855,12 @@ let check_rule_productivity l =
let is_not_printable onlyparse noninjective = function
| NVar _ ->
let () = if not onlyparse then
- msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
+ Feedback.msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
in
true
| _ ->
if not onlyparse && noninjective then
- let () = msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
+ let () = Feedback.msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
true
else onlyparse
@@ -886,7 +886,7 @@ let find_precedence lev etyps symbols =
| ETName | ETBigint | ETReference ->
begin match lev with
| None ->
- ([msg_info,strbrk "Setting notation at level 0."],0)
+ ([Feedback.msg_info,strbrk "Setting notation at level 0."],0)
| Some 0 ->
([],0)
| _ ->
@@ -904,7 +904,7 @@ let find_precedence lev etyps symbols =
else [],Option.get lev)
| Terminal _ when last_is_terminal () ->
if Option.is_empty lev then
- ([msg_info,strbrk "Setting notation at level 0."], 0)
+ ([Feedback.msg_info,strbrk "Setting notation at level 0."], 0)
else [],Option.get lev
| _ ->
if Option.is_empty lev then error "Cannot determine the level.";
@@ -931,7 +931,7 @@ let remove_curly_brackets l =
(match next' with
| Terminal "}" as t2 :: l'' as l1 ->
if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then
- msg_warning (strbrk "Skipping spaces inside curly brackets");
+ Feedback.msg_warning (strbrk "Skipping spaces inside curly brackets");
if deb && List.is_empty l'' then [t1;x;t2] else begin
check_curly_brackets_notation_exists ();
x :: aux false l''
@@ -976,7 +976,7 @@ let compute_pure_syntax_data df mods =
let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
let msgs =
if onlyparse then
- (msg_warning,
+ (Feedback.msg_warning,
strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
else msgs in
msgs, sy_data, extra
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index d0fa7a80c..36c16208c 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -146,7 +146,7 @@ let dir_ml_load s =
let dir_ml_use s =
match !load with
| WithTop t -> t.use_file s
- | _ -> msg_warning (str "Cannot access the ML compiler")
+ | _ -> Feedback.msg_warning (str "Cannot access the ML compiler")
(* Adds a path to the ML paths *)
let add_ml_dir s =
@@ -164,7 +164,7 @@ let add_rec_ml_dir unix_path =
let convert_string d =
try Names.Id.of_string d
with UserError _ ->
- msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
+ Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
raise Exit
let add_rec_path ~unix_path ~coq_root ~implicit =
@@ -184,7 +184,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
let () = List.iter add dirs in
Loadpath.add_load_path unix_path ~implicit coq_root
else
- msg_warning (str "Cannot open " ++ str unix_path)
+ Feedback.msg_warning (str "Cannot open " ++ str unix_path)
(* convertit un nom quelconque en nom de fichier ou de module *)
let mod_of_name name =
@@ -324,10 +324,10 @@ let if_verbose_load verb f name ?path fname =
let info = str "[Loading ML file " ++ str fname ++ str " ..." in
try
let path = f name ?path fname in
- msg_info (info ++ str " done]");
+ Feedback.msg_info (info ++ str " done]");
path
with reraise ->
- msg_info (info ++ str " failed]");
+ Feedback.msg_info (info ++ str " failed]");
raise reraise
(** Load a module for the first time (i.e. dynlink it)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 54baa5e3c..dbc3ccaac 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -24,7 +24,7 @@ let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
let trace s =
- if !Flags.debug then msg_debug s
+ if !Flags.debug then Feedback.msg_debug s
else ()
let succfix (depth, fixrels) =
@@ -731,11 +731,11 @@ type progress =
let obligations_message rem =
if rem > 0 then
if Int.equal rem 1 then
- Flags.if_verbose msg_info (int rem ++ str " obligation remaining")
+ Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining")
else
- Flags.if_verbose msg_info (int rem ++ str " obligations remaining")
+ Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining")
else
- Flags.if_verbose msg_info (str "No more obligations remaining")
+ Flags.if_verbose Feedback.msg_info (str "No more obligations remaining")
let update_obls prg obls rem =
let prg' = { prg with prg_obligations = (obls, rem) } in
@@ -992,7 +992,7 @@ and try_solve_obligations n tac =
try ignore (solve_obligations n tac) with NoObligations _ -> ()
and auto_solve_obligations n ?oblset tac : progress =
- Flags.if_verbose msg_info (str "Solving obligations automatically...");
+ Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically...");
try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
open Pp
@@ -1000,13 +1000,13 @@ let show_obligations_of_prg ?(msg=true) prg =
let n = prg.prg_name in
let obls, rem = prg.prg_obligations in
let showed = ref 5 in
- if msg then msg_info (int rem ++ str " obligation(s) remaining: ");
+ if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: ");
Array.iteri (fun i x ->
match x.obl_body with
| None ->
if !showed > 0 then (
decr showed;
- msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
+ Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
str "." ++ fnl ())))
@@ -1035,12 +1035,12 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
- Flags.if_verbose msg_info (info ++ str ".");
+ Flags.if_verbose Feedback.msg_info (info ++ str ".");
let cst = declare_definition prg in
Defined cst)
else (
let len = Array.length obls in
- let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
+ let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
progmap_add n (CEphemeron.create prg);
let res = auto_solve_obligations (Some n) tactic in
match res with
diff --git a/toplevel/record.ml b/toplevel/record.ml
index d12b5ee8e..0c3bd953c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -196,7 +196,7 @@ let warning_or_error coe indsp err =
(pr_id fi ++ strbrk " cannot be defined because it is not typable.")
in
if coe then errorlabstrm "structure" st;
- Flags.if_verbose msg_warning (hov 0 st)
+ Flags.if_verbose Feedback.msg_warning (hov 0 st)
type field_status =
| NoProjection of Name.t
@@ -262,7 +262,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
| Some None | None -> false
in
if not is_primitive then
- Flags.if_verbose msg_warning
+ Flags.if_verbose Feedback.msg_warning
(hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++
str" could not be defined as a primitive record"));
is_primitive
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 64225a644..1c3f0d997 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -119,8 +119,7 @@ let verbose_phrase verbch loc =
let s = String.create len in
seek_in ch (fst loc);
really_input ch s 0 len;
- ppnl (str s);
- pp_flush()
+ Feedback.msg_notice (str s ++ fnl ())
| None -> ()
exception End_of_input
@@ -152,9 +151,9 @@ let pr_new_syntax loc ocom =
| Some com -> Ppvernac.pr_vernac com
| None -> mt() in
if !beautify_file then
- msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
+ Feedback.msg_notice (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
else
- msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
+ Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
States.unfreeze fs;
Format.set_formatter_out_channel stdout
@@ -193,14 +192,15 @@ let display_cmd_header loc com =
with e -> str (Printexc.to_string e) in
let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
in
- Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
- str " [" ++ str cmd ++ str "] ");
- Pp.flush_all ()
+ Feedback.msg_notice
+ (str "Chars " ++ int start ++ str " - " ++ int stop ++
+ str " [" ++ str cmd ++ str "] ")
+
let rec vernac_com verbose checknav (loc,com) =
let interp = function
| VernacLoad (verbosely, fname) ->
- let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+ let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
let fname = CUnix.make_suffix fname ".v" in
let f = Loadpath.locate_file fname in
let st = save_translator_coqdoc () in
@@ -248,8 +248,7 @@ and read_vernac_file verbosely s =
* raised, which means that we raised the end of the file being loaded *)
while true do
let loc_ast = parse_sentence input in
- vernac_com verbosely checknav loc_ast;
- pp_flush ()
+ vernac_com verbosely checknav loc_ast
done
with any -> (* whatever the exception *)
let (e, info) = Errors.push any in
@@ -294,7 +293,7 @@ let load_vernac verb file =
let ensure_v f =
if Filename.check_suffix f ".v" then f
else begin
- msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
+ Feedback.msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
expanded to \"" ++ str f ++ str ".v\"");
f ^ ".v"
end
@@ -304,7 +303,7 @@ let compile verbosely f =
let check_pending_proofs () =
let pfs = Pfedit.get_all_proof_names () in
if not (List.is_empty pfs) then
- (msg_error (str "There are pending proofs"); flush_all (); exit 1) in
+ (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in
match !Flags.compilation_mode with
| BuildVo ->
let long_f_dot_v = ensure_v f in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 23755dac1..222b7d3df 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -57,7 +57,7 @@ let show_proof () =
(* spiwack: this would probably be cooler with a bit of polishing. *)
let p = Proof_global.give_me_the_proof () in
let pprf = Proof.partial_proof p in
- msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
+ Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
let show_node () =
(* spiwack: I'm have little clue what this function used to do. I deactivated it,
@@ -65,22 +65,22 @@ let show_node () =
()
let show_thesis () =
- msg_error (anomaly (Pp.str "TODO") )
+ Feedback.msg_error (anomaly (Pp.str "TODO") )
let show_top_evars () =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
let pfts = get_pftreestate () in
let gls = Proof.V82.subgoals pfts in
let sigma = gls.Evd.sigma in
- msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
+ Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
let show_universes () =
let pfts = get_pftreestate () in
let gls = Proof.V82.subgoals pfts in
let sigma = gls.Evd.sigma in
let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
- msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
- msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
+ Feedback.msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
+ Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
let show_prooftree () =
(* Spiwack: proof tree is currently not working *)
@@ -91,11 +91,10 @@ let enable_goal_printing = ref true
let print_subgoals () =
if !enable_goal_printing && is_verbose ()
then begin
- msg_notice (pr_open_subgoals ())
+ Feedback.msg_notice (pr_open_subgoals ())
end
let try_print_subgoals () =
- Pp.flush_all();
try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ()
@@ -109,10 +108,10 @@ let show_intro all =
let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
if all then
let lid = Tactics.find_intro_names l gl in
- msg_notice (hov 0 (prlist_with_sep spc pr_id lid))
+ Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid))
else if not (List.is_empty l) then
let n = List.last l in
- msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
+ Feedback.msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
end
(** Prepare a "match" template for a given inductive type.
@@ -153,7 +152,7 @@ let show_match id =
let pr_branch l =
str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
in
- msg_notice (v 1 (str "match # with" ++ fnl () ++
+ Feedback.msg_notice (v 1 (str "match # with" ++ fnl () ++
prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ()))
(* "Print" commands *)
@@ -194,23 +193,23 @@ let print_module r =
let globdir = Nametab.locate_dir qid in
match globdir with
DirModule (dirpath,(mp,_)) ->
- msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
+ Feedback.msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
| _ -> raise Not_found
with
- Not_found -> msg_error (str"Unknown Module " ++ pr_qualid qid)
+ Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid)
let print_modtype r =
let (loc,qid) = qualid_of_reference r in
try
let kn = Nametab.locate_modtype qid in
- msg_notice (Printmod.print_modtype kn)
+ Feedback.msg_notice (Printmod.print_modtype kn)
with Not_found ->
(* Is there a module of this name ? If yes we display its type *)
try
let mp = Nametab.locate_module qid in
- msg_notice (Printmod.print_module false mp)
+ Feedback.msg_notice (Printmod.print_module false mp)
with Not_found ->
- msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid)
+ Feedback.msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid)
let print_namespace ns =
let ns = List.rev (Names.DirPath.repr ns) in
@@ -279,7 +278,7 @@ let print_namespace ns =
acc
) constants (str"")
in
- msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace)
+ Feedback.msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace)
let print_strategy r =
let open Conv_oracle in
@@ -309,7 +308,7 @@ let print_strategy r =
else str "Constant strategies" ++ fnl () ++
hov 0 (prlist_with_sep fnl pr_strategy cst_lvl)
in
- msg_notice (var_msg ++ cst_msg)
+ Feedback.msg_notice (var_msg ++ cst_msg)
| Some r ->
let r = Smartlocate.smart_global r in
let key = match r with
@@ -318,7 +317,7 @@ let print_strategy r =
| IndRef _ | ConstructRef _ -> error "The reference is not unfoldable"
in
let lvl = get_strategy oracle key in
- msg_notice (pr_strategy (r, lvl))
+ Feedback.msg_notice (pr_strategy (r, lvl))
let dump_universes_gen g s =
let output = open_out s in
@@ -352,7 +351,7 @@ let dump_universes_gen g s =
try
UGraph.dump_universes output_constraint g;
close ();
- msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
+ Feedback.msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
with reraise ->
let reraise = Errors.push reraise in
close ();
@@ -367,11 +366,11 @@ let locate_file f =
let msg_found_library = function
| Library.LibLoaded, fulldir, file ->
- msg_info (hov 0
+ Feedback.msg_info (hov 0
(pr_dirpath fulldir ++ strbrk " has been loaded from file " ++
str file))
| Library.LibInPath, fulldir, file ->
- msg_info (hov 0
+ Feedback.msg_info (hov 0
(pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
let err_unmapped_library loc ?from qid =
@@ -506,7 +505,7 @@ let vernac_exact_proof c =
called only at the begining of a proof. *)
let status = by (Tactics.exact_proof c) in
save_proof (Vernacexpr.(Proved(Opaque None,None)));
- if not status then Pp.feedback Feedback.AddedAxiom
+ if not status then Feedback.feedback Feedback.AddedAxiom
let vernac_assumption locality poly (local, kind) l nl =
let local = enforce_locality_exp locality local in
@@ -518,7 +517,7 @@ let vernac_assumption locality poly (local, kind) l nl =
if global then Dumpglob.dump_definition lid false "ax"
else Dumpglob.dump_definition lid true "var") idl) l;
let status = do_assumptions kind nl l in
- if not status then Pp.feedback Feedback.AddedAxiom
+ if not status then Feedback.feedback Feedback.AddedAxiom
let vernac_record k poly finite struc binders sort nameopt cfs =
let const = match nameopt with
@@ -636,7 +635,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
id binders_ast (Enforce mty_ast) []
in
Dumpglob.dump_moddef loc mp "mod";
- if_verbose msg_info (str "Module " ++ pr_id id ++ str " is declared");
+ if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -657,7 +656,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
export id binders_ast mty_ast_o
in
Dumpglob.dump_moddef loc mp "mod";
- if_verbose msg_info
+ if_verbose Feedback.msg_info
(str "Interactive Module " ++ pr_id id ++ str " started");
List.iter
(fun (export,id) ->
@@ -675,7 +674,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
id binders_ast mty_ast_o mexpr_ast_l
in
Dumpglob.dump_moddef loc mp "mod";
- if_verbose msg_info
+ if_verbose Feedback.msg_info
(str "Module " ++ pr_id id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)])
export
@@ -683,7 +682,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
let vernac_end_module export (loc,id as lid) =
let mp = Declaremods.end_module () in
Dumpglob.dump_modref loc mp "mod";
- if_verbose msg_info (str "Module " ++ pr_id id ++ str " is defined");
+ if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident lid]) export
let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -704,7 +703,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
id binders_ast mty_sign
in
Dumpglob.dump_moddef loc mp "modtype";
- if_verbose msg_info
+ if_verbose Feedback.msg_info
(str "Interactive Module Type " ++ pr_id id ++ str " started");
List.iter
(fun (export,id) ->
@@ -723,13 +722,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
id binders_ast mty_sign mty_ast_l
in
Dumpglob.dump_moddef loc mp "modtype";
- if_verbose msg_info
+ if_verbose Feedback.msg_info
(str "Module Type " ++ pr_id id ++ str " is defined")
let vernac_end_modtype (loc,id) =
let mp = Declaremods.end_modtype () in
Dumpglob.dump_modref loc mp "modtype";
- if_verbose msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
+ if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
let vernac_include l =
Declaremods.declare_include Modintern.interp_module_ast l
@@ -797,7 +796,7 @@ let vernac_coercion locality poly local ref qids qidt =
let source = cl_of_qualid qids in
let ref' = smart_global ref in
Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target;
- if_verbose msg_info (pr_global ref' ++ str " is now a coercion")
+ if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
let vernac_identity_coercion locality poly local id qids qidt =
let local = enforce_locality locality local in
@@ -813,7 +812,7 @@ let vernac_instance abst locality poly sup inst props pri =
ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
let vernac_context poly l =
- if not (Classes.context poly l) then Pp.feedback Feedback.AddedAxiom
+ if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
let vernac_declare_instances locality ids pri =
let glob = not (make_section_locality locality) in
@@ -869,7 +868,7 @@ let vernac_set_used_variables e =
(* Auxiliary file management *)
let expand filename =
- Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename
+ Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
let vernac_add_loadpath implicit pdir ldiropt =
let pdir = expand pdir in
@@ -889,13 +888,13 @@ let vernac_declare_ml_module locality l =
Mltop.declare_ml_modules local (List.map expand l)
let vernac_chdir = function
- | None -> msg_notice (str (Sys.getcwd()))
+ | None -> Feedback.msg_notice (str (Sys.getcwd()))
| Some path ->
begin
try Sys.chdir (expand path)
- with Sys_error err -> msg_warning (str "Cd failed: " ++ str err)
+ with Sys_error err -> Feedback.msg_warning (str "Cd failed: " ++ str err)
end;
- if_verbose msg_info (str (Sys.getcwd()))
+ if_verbose Feedback.msg_info (str (Sys.getcwd()))
(********************)
@@ -1068,7 +1067,7 @@ let vernac_declare_arguments locality r l nargs flags =
some_scopes_specified ||
some_simpl_flags_specified) &&
no_flags then
- msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'")
+ Feedback.msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'")
let default_env () = {
@@ -1423,7 +1422,7 @@ let vernac_check_may_eval redexp glopt rc =
| None ->
let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
- msg_notice (print_judgment env sigma' j ++
+ Feedback.msg_notice (print_judgment env sigma' j ++
pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
Printer.pr_universe_ctx sigma uctx)
| Some r ->
@@ -1434,7 +1433,7 @@ let vernac_check_may_eval redexp glopt rc =
let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in
c
in
- msg_notice (print_eval redfun env sigma' rc j)
+ Feedback.msg_notice (print_eval redfun env sigma' rc j)
let vernac_declare_reduction locality s r =
let local = make_locality locality in
@@ -1450,7 +1449,7 @@ let vernac_global_check c =
let senv = Safe_typing.add_constraints cstrs senv in
let j = Safe_typing.typing senv c in
let env = Safe_typing.env_of_safe_env senv in
- msg_notice (print_safe_judgment env sigma j)
+ Feedback.msg_notice (print_safe_judgment env sigma j)
let get_nth_goal n =
@@ -1487,7 +1486,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
| NoHyp | Not_found -> print_about ref_or_by_not
-let vernac_print = function
+let vernac_print = let open Feedback in function
| PrintTables -> msg_notice (print_tables ())
| PrintFullContext-> msg_notice (print_full_context_typ ())
| PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
@@ -1586,6 +1585,7 @@ let vernac_search s gopt r =
| Some g -> snd (Pfedit.get_goal_context g) , Some g
in
let get_pattern c = snd (intern_constr_pattern env c) in
+ let open Feedback in
match s with
| SearchPattern c ->
msg_notice (Search.search_pattern gopt (get_pattern c) r)
@@ -1596,8 +1596,8 @@ let vernac_search s gopt r =
| SearchAbout sl ->
msg_notice (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r)
-let vernac_locate = function
- | LocateAny (AN qid) -> msg_notice (print_located_qualid qid)
+let vernac_locate = let open Feedback in function
+ | LocateAny (AN qid) -> msg_notice (print_located_qualid qid)
| LocateTerm (AN qid) -> msg_notice (print_located_term qid)
| LocateAny (ByNotation (_, ntn, sc)) (** TODO : handle Ltac notations *)
| LocateTerm (ByNotation (_, ntn, sc)) ->
@@ -1640,7 +1640,7 @@ let vernac_unfocus () =
let vernac_unfocused () =
let p = Proof_global.give_me_the_proof () in
if Proof.unfocused p then
- msg_notice (str"The proof is indeed fully unfocused.")
+ Feedback.msg_notice (str"The proof is indeed fully unfocused.")
else
error "The proof is not fully unfocused."
@@ -1668,7 +1668,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) =
Proof_global.simple_with_current_proof (fun _ p ->
Proof_global.Bullet.put p bullet)
-let vernac_show = function
+let vernac_show = let open Feedback in function
| ShowGoal goalref ->
let info = match goalref with
| OpenSubgoals -> pr_open_subgoals ()
@@ -1706,7 +1706,7 @@ let vernac_check_guard () =
with UserError(_,s) ->
(str ("Condition violated: ") ++s)
in
- msg_notice message
+ Feedback.msg_notice message
exception End_of_input
@@ -1717,7 +1717,7 @@ let vernac_load interp fname =
| Some x -> x
| None -> raise End_of_input) in
let fname =
- Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+ Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
let fname = CUnix.make_suffix fname ".v" in
let input =
let longfname = Loadpath.locate_file fname in
@@ -1849,15 +1849,15 @@ let interp ?proof ~loc locality poly c =
| VernacSearch (s,g,r) -> vernac_search s g r
| VernacLocate l -> vernac_locate l
| VernacRegister (id, r) -> vernac_register id r
- | VernacComments l -> if_verbose msg_info (str "Comments ok\n")
+ | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
(* The STM should handle that, but LOAD bypasses the STM... *)
- | VernacAbort id -> msg_warning (str "VernacAbort not handled by Stm")
- | VernacAbortAll -> msg_warning (str "VernacAbortAll not handled by Stm")
- | VernacRestart -> msg_warning (str "VernacRestart not handled by Stm")
- | VernacUndo _ -> msg_warning (str "VernacUndo not handled by Stm")
- | VernacUndoTo _ -> msg_warning (str "VernacUndoTo not handled by Stm")
- | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm")
+ | VernacAbort id -> Feedback.msg_warning (str "VernacAbort not handled by Stm")
+ | VernacAbortAll -> Feedback.msg_warning (str "VernacAbortAll not handled by Stm")
+ | VernacRestart -> Feedback.msg_warning (str "VernacRestart not handled by Stm")
+ | VernacUndo _ -> Feedback.msg_warning (str "VernacUndo not handled by Stm")
+ | VernacUndoTo _ -> Feedback.msg_warning (str "VernacUndoTo not handled by Stm")
+ | VernacBacktrack _ -> Feedback.msg_warning (str "VernacBacktrack not handled by Stm")
(* Proof management *)
| VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
@@ -1991,7 +1991,7 @@ let with_fail b f =
| HasNotFailed ->
errorlabstrm "Fail" (str "The command has not failed!")
| HasFailed msg ->
- if is_verbose () || !test_mode || !ide_slave then msg_info
+ if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
| _ -> assert false
end
@@ -2016,7 +2016,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
current_timeout := Some n;
aux ?locality ?polymorphism isprogcmd v
| VernacRedirect (s, (_,v)) ->
- Pp.with_output_to_file s (aux false) v
+ Feedback.with_output_to_file s (aux false) v
| VernacTime (_,v) ->
System.with_time !Flags.time
(aux ?locality ?polymorphism isprogcmd) v;
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 7fbd2b119..1116a3104 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -55,7 +55,7 @@ let call ?locality (opn,converted_args) =
| Egramml.GramNonTerminal _ -> str "_"
in
let pr = pr_sequence pr_gram rules in
- msg_warning (str "Deprecated vernacular command: " ++ pr)
+ Feedback.msg_warning (str "Deprecated vernacular command: " ++ pr)
in
loc:= "Checking arguments";
let hunk = callback converted_args in
@@ -68,5 +68,5 @@ let call ?locality (opn,converted_args) =
| reraise ->
let reraise = Errors.push reraise in
if !Flags.debug then
- msg_debug (str"Vernac Interpreter " ++ str !loc);
+ Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc);
iraise reraise
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 05:48:12 +0000