From dfd97b1229e856e7d7fbdd5e11ddf60707d05ae0 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 1 Jun 2006 10:51:34 +0000 Subject: [PATCH] made pp_term parametric and explained the proper way of solving the object pretty printing problem --- components/acic_content/cicNotationPp.ml | 4 +++- components/acic_content/cicNotationPp.mli | 18 ++++++++++++++++++ 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml index fb38674df..5f45b2a4b 100644 --- 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 57a4d6b82..2e60c7444 100644 --- 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 + -- 2.39.2