]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationRew.ml
All the debug_print are now lazy.
[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml
index d65eb0a5047724e1c49e2b8ee8408523e1a4c7bb..3d684fe39b0ff27f57fd3eb6cd23180d30042f20 100644 (file)
@@ -28,7 +28,7 @@ open Printf
 module Ast = CicNotationPt
 
 let debug = false
-let debug_print = if debug then prerr_endline else ignore
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 type pattern_id = int
 type interpretation_id = pattern_id
@@ -567,17 +567,17 @@ let load_patterns21 t =
   set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t))
 
 let ast_of_acic id_to_sort annterm =
-  debug_print ("ast_of_acic <- "
-    ^ CicPp.ppterm (Deannotate.deannotate_term annterm));
+  debug_print (lazy ("ast_of_acic <- "
+    ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
   let ast = ast_of_acic1 term_info annterm in
-  debug_print ("ast_of_acic -> " ^ CicNotationPp.pp_term ast);
+  debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
   ast, term_info.uri
 
 let pp_ast ast =
-  debug_print "pp_ast <-";
+  debug_print (lazy "pp_ast <-");
   let ast' = pp_ast1 ast in
-  debug_print ("pp_ast -> " ^ CicNotationPp.pp_term ast');
+  debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast'));
   ast'
 
 let fresh_id =