- let cb status stm =
- (* dump_status status; *)
- let stm = TacticAstPp.pp_statement stm in
- let stm = Pcre.replace ~rex:slash_n_RE stm in
- let stm =
- if String.length stm > 50 then
- String.sub stm 0 50 ^ " ..."
- else
- stm
- in
- MatitaLog.debug ("Executing: ``" ^ stm ^ "''")
+ let cb =
+ if Helm_registry.get_bool "matita.quiet" then
+ (fun _ _ -> ())
+ else
+ (fun status stm ->
+ (* dump_status status; *)
+ let stm = GrafiteAstPp.pp_statement stm in
+ let stm = Pcre.replace ~rex:slash_n_RE stm in
+ let stm =
+ if String.length stm > 50 then
+ String.sub stm 0 50 ^ " ..."
+ else
+ stm
+ in
+ MatitaLog.debug ("Executing: ``" ^ stm ^ "''"))