diff options
author | 2017-03-30 14:58:12 +0200 | |
---|---|---|
committer | 2017-04-12 16:49:46 +0200 | |
commit | cf24cedb2926fa00db222eeac48e88a6078b4444 (patch) | |
tree | 649354ba1da3c3747f1e30c1a6d1f32dd5b2b470 /stm/stm.ml | |
parent | 2f0a56562112c4bd66082fb3eafffb8cf6f03a88 (diff) |
[stm] [nit] Centralize compile-time debug flag.
Diffstat (limited to 'stm/stm.ml')
-rw-r--r-- | stm/stm.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index d11aea6c4..574426f92 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -6,13 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* enable in case of stm problems *) +let stm_debug = false + let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr -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 () +let stm_prerr_endline s = if stm_debug then begin stm_pr_err (s ()) end else () +let stm_pperr_endline s = if stm_debug then begin stm_pp_err (s ()) end else () -let stm_pperr_endline s = if false then begin stm_pp_err (s ()) end else () +let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () open Vernacexpr open CErrors @@ -2678,7 +2681,7 @@ let parse_sentence sid pa = (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ; - if not (Stateid.equal sid real_tip) then + if not (Stateid.equal sid real_tip) && !Flags.debug && stm_debug then Feedback.msg_debug (str "Warning, the real tip doesn't match the current tip." ++ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ |