From 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Dec 2016 12:12:54 +0100 Subject: [pp] [ide] Minor cleanups in pp code. - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics. --- ide/coqOps.ml | 30 ++++++++++++++----------- ide/ideutils.ml | 2 +- ide/minilib.ml | 6 +++-- ide/minilib.mli | 3 ++- lib/pp.ml | 2 ++ lib/pp.mli | 3 +++ library/summary.ml | 6 +++-- proofs/proof_global.ml | 4 ++-- proofs/proof_using.ml | 2 +- stm/asyncTaskQueue.ml | 25 ++++++++++----------- stm/stm.ml | 58 ++++++++++++++++++++++++------------------------- vernac/auto_ind_decl.ml | 4 ++-- vernac/vernacentries.ml | 4 ++-- 13 files changed, 81 insertions(+), 68 deletions(-) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index cee243f91..1b4c5d3be 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -128,6 +128,9 @@ end = struct end open SentenceId +let log_pp msg : unit task = + Coq.lift (fun () -> Minilib.log_pp msg) + let log msg : unit task = Coq.lift (fun () -> Minilib.log msg) @@ -308,7 +311,7 @@ object(self) method private print_stack = Minilib.log "document:"; - Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer))) + Minilib.log_pp (Doc.print document (dbg_to_string buffer)) method private enter_focus start stop = let at id id' _ = Stateid.equal id' id in @@ -379,8 +382,7 @@ object(self) Coq.bind (Coq.seq action query) next method private mark_as_needed sentence = - Minilib.log("Marking " ^ - Pp.string_of_ppcmds (dbg_to_string buffer false None sentence)); + Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence); let start = buffer#get_iter_at_mark sentence.start in let stop = buffer#get_iter_at_mark sentence.stop in let to_process = Tags.Script.to_process in @@ -437,9 +439,11 @@ object(self) | _ -> None in try Some (Doc.find_map document finder) with Not_found -> None in - let log s state_id = - Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string - (Option.default Stateid.dummy state_id)) in + let log_pp s state_id = + Minilib.log_pp Pp.(seq + [str "Feedback "; s; str " on "; + str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in + let log s state_id = log_pp (Pp.str s) state_id in begin match msg.contents, sentence with | AddedAxiom, Some (id,sentence) -> log "AddedAxiom" id; @@ -469,24 +473,24 @@ object(self) (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let msg = Pp.string_of_ppcmds msg in - log "ErrorMsg" id; + log_pp Pp.(str "ErrorMsg" ++ msg) id; remove_flag sentence `PROCESSING; - add_flag sentence (`ERROR (loc, msg)); + let rmsg = Pp.string_of_ppcmds msg in + add_flag sentence (`ERROR (loc, rmsg)); self#mark_as_needed sentence; - self#attach_tooltip sentence loc msg; + self#attach_tooltip sentence loc rmsg; if not (Loc.is_ghost loc) then self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) | Message(Warning, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let rmsg = Pp.string_of_ppcmds msg in - log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id; + log_pp Pp.(str "WarningMsg" ++ msg) id; + let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`WARNING (loc, rmsg)); self#attach_tooltip sentence loc rmsg; self#position_warning_tag_at_sentence sentence loc; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> - log ("Msg: " ^ Pp.string_of_ppcmds msg) id; + log_pp Pp.(str "Msg" ++ msg) id; messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 101f1a5ee..da867e689 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -337,7 +337,7 @@ let default_logger level message = | Feedback.Warning -> `WARNING | Feedback.Error -> `ERROR in - Minilib.log ~level (Pp.string_of_ppcmds message) + Minilib.log_pp ~level message (** {6 File operations} *) diff --git a/ide/minilib.ml b/ide/minilib.ml index d11e8c56b..2c24e46f8 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -30,7 +30,7 @@ let debug = ref false print in the response buffer. *) -let log ?(level = `DEBUG) msg = +let log_pp ?(level = `DEBUG) msg = let prefix = match level with | `DEBUG -> "DEBUG" | `INFO -> "INFO" @@ -40,10 +40,12 @@ let log ?(level = `DEBUG) msg = | `FATAL -> "FATAL" in if !debug then begin - try Printf.eprintf "[%s] %s\n%!" prefix msg + try Format.eprintf "[%s] @[%a@]\n%!" prefix Pp.pp_with msg with _ -> () end +let log ?level str = log_pp ?level (Pp.str str) + let coqify d = Filename.concat d "coq" let coqide_config_home () = diff --git a/ide/minilib.mli b/ide/minilib.mli index b7672c900..4517a2374 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,7 +22,8 @@ type level = [ (** debug printing *) val debug : bool ref -val log : ?level:level -> string -> unit +val log_pp : ?level:level -> Pp.std_ppcmds -> unit +val log : ?level:level -> string -> unit val coqide_config_home : unit -> string val coqide_config_dirs : unit -> string list diff --git a/lib/pp.ml b/lib/pp.ml index 7b21f9bbd..80c599274 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -77,6 +77,8 @@ let app s1 s2 = match s1, s2 with | s, Ppcmd_empty -> s | s1, s2 -> Ppcmd_glue [s1; s2] +let seq s = Ppcmd_glue s + let (++) = app (* formatting commands *) diff --git a/lib/pp.mli b/lib/pp.mli index 2c45ce0a7..4b7ac5c1a 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -68,6 +68,9 @@ val comment : string list -> std_ppcmds val app : std_ppcmds -> std_ppcmds -> std_ppcmds (** Concatenation. *) +val seq : std_ppcmds list -> std_ppcmds +(** Multi-Concatenation. *) + val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds (** Infix alias for [app]. *) diff --git a/library/summary.ml b/library/summary.ml index 6efa07f38..2ec4760d6 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -107,8 +107,10 @@ let unfreeze_summaries fs = try fold id decl state with e when CErrors.noncritical e -> let e = CErrors.push e in - Printf.eprintf "Error unfrezing summay %s\n%s\n%!" - (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e)); + Feedback.msg_error + Pp.(seq [str "Error unfrezing summay %s\n%s\n%!"; + str (name_of_summary id); + CErrors.iprint e]); iraise e in (** We rely on the order of the frozen list, and the order of folding *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 120cde5e5..ca7330fdb 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -195,9 +195,9 @@ let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - CErrors.error (Pp.string_of_ppcmds + CErrors.user_err (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++ - str"Use \"Abort All\" first or complete proof(s).")) + str"Use \"Abort All\" first or complete proof(s).") end let discard_gen id = diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index a125fb10d..f51586c73 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids = let suggest_Proof_using name env vars ids_typ context_ids = let module S = Id.Set in let open Pp in - let print x = prerr_endline (string_of_ppcmds x) in + let print x = Feedback.msg_error x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 28548ecee..125491988 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -10,9 +10,9 @@ open CErrors open Pp open Util -let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () type 'a worker_status = [ `Fresh | `Old of 'a ] @@ -147,23 +147,23 @@ module Make(T : Task) = struct let stop_waiting = ref false in let expiration_date = ref (ref false) in let pick_task () = - prerr_endline "waiting for a task"; + stm_prerr_endline "waiting for a task"; let pick age (t, c) = not !c && T.task_match age t in let task, task_expiration = TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in expiration_date := task_expiration; last_task := Some task; - prerr_endline ("got task: "^T.name_of_task task); + stm_prerr_endline ("got task: " ^ T.name_of_task task); task in let add_tasks l = List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in let get_exec_token () = ignore(CoqworkmgrApi.get 1); got_token := true; - prerr_endline ("got execution token") in + stm_prerr_endline ("got execution token") in let kill proc = Worker.kill proc; - prerr_endline ("Worker exited: " ^ + stm_prerr_endline ("Worker exited: " ^ match Worker.wait proc with | Unix.WEXITED 0x400 -> "exit code unavailable" | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i @@ -196,7 +196,7 @@ module Make(T : Task) = struct report_status ~id "Idle"; let task = pick_task () in match T.request_of_task !worker_age task with - | None -> prerr_endline ("Task expired: " ^ T.name_of_task task) + | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task) | Some req -> try get_exec_token (); @@ -222,8 +222,7 @@ module Make(T : Task) = struct raise e (* we pass the exception to the external handler *) | MarshalError s -> T.on_marshal_error s task; raise Die | e -> - pr_err ("Uncaught exception in worker manager: "^ - string_of_ppcmds (print e)); + stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]); flush_all (); raise Die done with | (Die | TQueue.BeingDestroyed) -> @@ -261,7 +260,7 @@ module Make(T : Task) = struct let broadcast { queue } = TQueue.broadcast queue let enqueue_task { queue; active } (t, _ as item) = - prerr_endline ("Enqueue task "^T.name_of_task t); + stm_prerr_endline ("Enqueue task "^T.name_of_task t); TQueue.push queue item let cancel_worker { active } n = Pool.cancel n active @@ -329,11 +328,11 @@ module Make(T : Task) = struct CEphemeron.clear () with | MarshalError s -> - pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 + stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2 | End_of_file -> - prerr_endline "connection lost"; flush_all (); exit 2 + stm_prerr_endline "connection lost"; flush_all (); exit 2 | e -> - pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e)); + stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]); flush_all (); exit 1 done diff --git a/stm/stm.ml b/stm/stm.ml index 75872d633..ee142b293 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr -let prerr_endline s = if false then begin pr_err (s ()) end else () -let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else () +let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else () +let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () open Vernacexpr open CErrors @@ -540,7 +540,7 @@ end = struct (* {{{ *) let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in checkout branch; - prerr_endline (fun () -> "mode:" ^ mode); + stm_prerr_endline (fun () -> "mode:" ^ mode); Proof_global.activate_proof_mode mode with Failure _ -> checkout Branch.master; @@ -852,7 +852,7 @@ end = struct (* {{{ *) if is_cached id && not redefine then anomaly (str"defining state "++str str_id++str" twice"); try - prerr_endline (fun () -> "defining "^str_id^" (cache="^ + stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); let good_id = match safe_id with None -> !cur_id | Some id -> id in fix_exn_ref := exn_on id ~valid:good_id; @@ -860,7 +860,7 @@ end = struct (* {{{ *) fix_exn_ref := (fun x -> x); if cache = `Yes then freeze `No id else if cache = `Shallow then freeze `Shallow id; - prerr_endline (fun () -> "setting cur id to "^str_id); + stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then Hooks.(call state_computed id ~in_cache:false); @@ -994,11 +994,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = in let aux_interp cmd = if is_filtered_command cmd then - prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) + stm_prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) else match cmd with | VernacShow ShowScript -> ShowScript.show_script () | expr -> - prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); + stm_prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) with e -> let e = CErrors.push e in @@ -1431,8 +1431,8 @@ end = struct (* {{{ *) | Some (safe, err) -> err, safe | None -> Stateid.dummy, Stateid.dummy in let e_msg = iprint (e, info) in - prerr_endline (fun () -> "failed with the following exception:"); - prerr_endline (fun () -> string_of_ppcmds e_msg); + stm_prerr_endline (fun () -> "failed with the following exception:"); + stm_prerr_endline (fun () -> string_of_ppcmds e_msg); let e_safe_states = List.filter State.is_cached_and_valid my_states in RespError { e_error_at; e_safe_id; e_msg; e_safe_states } @@ -1697,7 +1697,7 @@ end = struct (* {{{ *) | Some (ReqBuildProof (r, b, _)) -> Some(r, b) | _ -> None) tasks in - prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs)); + stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs)); reqs let reset_task_queue () = TaskQueue.clear (Option.get !queue) @@ -1781,7 +1781,7 @@ end = struct (* {{{ *) `Stay ((),[]) let on_marshal_error err { t_name } = - pr_err ("Fatal marshal error: " ^ t_name ); + stm_pr_err ("Fatal marshal error: " ^ t_name ); flush_all (); exit 1 let on_task_cancellation_or_expiration_or_slave_death = function @@ -1880,7 +1880,7 @@ end = struct (* {{{ *) let open Notations in try let pt, uc = Future.join f in - prerr_endline (fun () -> string_of_ppcmds(hov 0 ( + stm_prerr_endline (fun () -> string_of_ppcmds(hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ str"uc=" ++ Evd.pr_evar_universe_context uc))); @@ -1925,7 +1925,7 @@ end = struct (* {{{ *) let use_response _ _ _ = `End let on_marshal_error _ _ = - pr_err ("Fatal marshal error in query"); + stm_pr_err ("Fatal marshal error in query"); flush_all (); exit 1 let on_task_cancellation_or_expiration_or_slave_death _ = () @@ -2000,7 +2000,7 @@ let warn_deprecated_nested_proofs = "stop working in a future Coq version")) let collect_proof keep cur hd brkind id = - prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); + stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in let name = function | [] -> no_name @@ -2100,7 +2100,7 @@ let string_of_reason = function | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section" | `Unknown -> "unsupported case" -let log_string s = prerr_debug (fun () -> "STM: " ^ s) +let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s) let log_processing_async id name = log_string Printf.(sprintf "%s: proof %s: asynch" (Stateid.to_string id) name ) @@ -2187,16 +2187,16 @@ let known_state ?(redefine_qed=false) ~cache id = Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id -> - prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); reach ~safe_id id; cherry_pick_non_pstate ()) id (* traverses the dag backward from nodes being already calculated *) and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = - prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin Hooks.(call state_computed id ~in_cache:true); - prerr_endline (fun () -> "reached (cache)"); + stm_prerr_endline (fun () -> "reached (cache)"); State.install_cached id end else let step, cache_step, feedback_processed = @@ -2348,7 +2348,7 @@ let known_state ?(redefine_qed=false) ~cache id = else cache_step in State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; - prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in + stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in reach ~redefine_qed id end (* }}} *) @@ -2363,7 +2363,7 @@ let init () = Backtrack.record (); Slaves.init (); if Flags.async_proofs_is_master () then begin - prerr_endline (fun () -> "Initializing workers"); + stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); let opts = match !Flags.async_proofs_private_flags with | None -> [] @@ -2415,9 +2415,9 @@ let rec join_admitted_proofs id = let join () = finish (); wait (); - prerr_endline (fun () -> "Joining the environment"); + stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); - prerr_endline (fun () -> "Joining Admitted proofs"); + stm_prerr_endline (fun () -> "Joining Admitted proofs"); join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); VCS.print (); VCS.print () @@ -2491,7 +2491,7 @@ let handle_failure (e, info) vcs tty = anomaly(str"error with no safe_id attached:" ++ spc() ++ CErrors.iprint_no_report (e, info)) | Some (safe_id, id) -> - prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; if tty && interactive () = `Yes then begin (* We stay on a valid state *) @@ -2514,13 +2514,13 @@ let reset_task_queue = Slaves.reset_task_queue (* Document building *) let process_transaction ?(newtip=Stateid.fresh ()) ~tty ({ verbose; loc; expr } as x) c = - prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); + stm_prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); let vcs = VCS.backup () in try let head = VCS.current_branch () in VCS.checkout head; let rc = begin - prerr_endline (fun () -> + stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with (* PG stuff *) @@ -2558,7 +2558,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> - prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); Reach.known_state ~cache:(interactive ()) id; `Ok @@ -2708,7 +2708,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty expr = VernacShow (ShowGoal OpenSubgoals) } | _ -> () end; - prerr_endline (fun () -> "processed }}}"); + stm_prerr_endline (fun () -> "processed }}}"); VCS.print (); rc with e -> @@ -2894,7 +2894,7 @@ let edit_at id = anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ CErrors.print_no_report e) | Some (_, id) -> - prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; VCS.print (); iraise (e, info) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 594f2e944..6d71601cc 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -444,14 +444,14 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = string_of_ppcmds + let err_msg = (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ Printer.pr_constr tt1 ++ str " first.") in - error err_msg + user_err err_msg in let bl_args = Array.append (Array.append (Array.map (fun x -> x) v) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 09c43f93e..999fe297e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -39,7 +39,7 @@ module NamedDecl = Context.Named.Declaration let (f_interp_redexp, interp_redexp_hook) = Hook.make () let debug = false -let prerr_endline x = +let vernac_prerr_endline x = if debug then prerr_endline (x ()) else () (* Misc *) @@ -1933,7 +1933,7 @@ let vernac_load interp fname = * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) let interp ?proof ~loc locality poly c = - prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); + vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* The below vernac are candidates for removal from the main type and to be put into a new doc_command datatype: *) -- cgit v1.2.3