diff options
| author | Enrico Tassi | 2014-02-26 15:28:53 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-02-26 15:28:53 +0100 |
| commit | 64c53a3045187d766b379e9b0902912e0c0d310d (patch) | |
| tree | 09fc72fc8ad4d39531bdfd59ad3fde1c80084503 | |
| parent | 9c4919bc7959f9990c9ef2019c79fde12dbae328 (diff) | |
STM: better debug messages
| -rw-r--r-- | toplevel/stm.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 399205189b..12c5cafd7f 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -572,7 +572,7 @@ end = struct (* {{{ *) anomaly (str"defining state "++str str_id++str" twice"); try prerr_endline("defining "^str_id^" (cache="^ - if cache = `Yes then "Y" else if cache = `Shallow then "S" else "N"); + if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); f (); if cache = `Yes then freeze `No id else if cache = `Shallow then freeze `Shallow id; @@ -1675,7 +1675,7 @@ let process_transaction ~tty verbose c (loc, expr) = let warn_if_pos a b = if b then msg_warning(pr_ast a ++ str" should not be part of a script") in let v, x = expr, { verbose = verbose && Flags.is_verbose(); loc; expr } in - prerr_endline ("{{{ execute: "^ string_of_ppcmds (pr_ast x)); + prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x)); let vcs = VCS.backup () in try let head = VCS.current_branch () in @@ -1821,7 +1821,7 @@ let process_transaction ~tty verbose c (loc, expr) = expr = VernacShow (ShowGoal OpenSubgoals) } | _ -> () end; - prerr_endline "executed }}}"; + prerr_endline "processed }}}"; VCS.print (); rc with e -> |