made pp_term parametric and explained the proper way of solving the object pretty...

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index fb38674dfb2cce12e406af6ab3b985b4964ffa8e..5f45b2a4ba72d23ea6f942d6124357578f3b2508 100644 (file)
--- a/components/acic_content/cicNotationPp.ml
+++ b/components/acic_content/cicNotationPp.ml
@@ -239,7 +239,9 @@ and pp_variable = function
   | Ast.Ascription (t, n) -> assert false
   | Ast.FreshVar n -> "fresh " ^ n
 
-let pp_term t = pp_term ~pp_parens:false t
+let _pp_term = ref (pp_term ~pp_parens:false)
+let pp_term t = !_pp_term t
+let set_pp_term f = _pp_term := f
 
 let pp_params = function
   | [] -> ""

diff --git a/components/acic_content/cicNotationPp.mli b/components/acic_content/cicNotationPp.mli
index 57a4d6b829238267471ce601dc1ced85a9118db9..2e60c74446cc207ed269304801686652906983bb 100644 (file)
--- a/components/acic_content/cicNotationPp.mli
+++ b/components/acic_content/cicNotationPp.mli
@@ -23,6 +23,21 @@
  * http://helm.cs.unibo.it/
  *)
 
+(** ZACK
+ * This module does not print terms and object properly, it has been created
+ * mainly for debugging reason. There is no guarantee that printed strings are
+ * re-parsable. Moreover, actually there is no way at all to proper print
+ * objects in a way that is re-parsable.
+ *
+ * TODO the proper implementation of a pp_obj function like the one below should
+ * be as follows. Change its type to
+ *  pp_obj: CicNotationPt.obj -> CicNotationPres.markup
+ * and parametrize it over a function with the following type
+ *  pp_term: CicNotationPt.term -> CicNotationPres.markup
+ * The obtained markup can then be printed using CicNotationPres.print_xml or
+ * BoxPp.render_to_string(s)
+ *)
+
 val pp_term: CicNotationPt.term -> string
 val pp_obj: CicNotationPt.obj -> string
 
@@ -35,3 +50,6 @@ val pp_attribute: CicNotationPt.term_attribute -> string
 
 val pp_cic_appl_pattern: CicNotationPt.cic_appl_pattern -> string
 
+ (** non re-entrant change of pp_term function above *)
+val set_pp_term: (CicNotationPt.term -> string) -> unit
+