From cbbd875911a596cbd7dd5247479cd967a88b0aa7 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 8 Feb 2007 16:44:53 +0000
Subject: [PATCH] Important commit: from now on the pretty printer
 CicMetaSubst.ppterm_in_context is substituted with a reference to an high
 level pretty-printer (now defined in matita/applyTransformation.ml). In the
 debug menu there is a switch to turn it off and get back the old
 pretty-printer.

---
 components/cic_unification/cicMetaSubst.ml  | 11 +++++++++++
 components/cic_unification/cicMetaSubst.mli |  4 ++++
 matita/applyTransformation.ml               | 16 ++++++++++++++++
 matita/matita.ml                            |  4 ++++
 4 files changed, 35 insertions(+)

diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml
index c097eacf2..a86bc471a 100644
--- a/components/cic_unification/cicMetaSubst.ml
+++ b/components/cic_unification/cicMetaSubst.ml
@@ -305,6 +305,17 @@ let ppterm_in_context ~metasenv subst term context =
  in
   ppterm_in_name_context ~metasenv subst term name_context
 
+let ppterm_in_context_ref = ref ppterm_in_context
+let set_ppterm_in_context f =
+ ppterm_in_context_ref := f
+let use_low_level_ppterm_in_context = ref false
+
+let ppterm_in_context ~metasenv subst term context =
+ if !use_low_level_ppterm_in_context then
+  ppterm_in_context ~metasenv subst term context
+ else
+  !ppterm_in_context_ref ~metasenv subst term context
+
 let ppcontext' ~metasenv ?(sep = "\n") subst context =
  let separate s = if s = "" then "" else s ^ sep in
   List.fold_right 
diff --git a/components/cic_unification/cicMetaSubst.mli b/components/cic_unification/cicMetaSubst.mli
index 2b60b04e0..bc5b4c039 100644
--- a/components/cic_unification/cicMetaSubst.mli
+++ b/components/cic_unification/cicMetaSubst.mli
@@ -60,6 +60,10 @@ val delift_rels :
   Cic.term * Cic.substitution * Cic.metasenv
  
 (** {2 Pretty printers} *)
+val use_low_level_ppterm_in_context : bool ref
+val set_ppterm_in_context :
+ (metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context ->
+   string) -> unit
 
 val ppsubst_unfolded: metasenv:Cic.metasenv -> Cic.substitution -> string
 val ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string
diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index 0678887ce..920d1fef4 100644
--- a/matita/applyTransformation.ml
+++ b/matita/applyTransformation.ml
@@ -97,6 +97,22 @@ let txt_of_cic_sequent_conclusion size metasenv sequent =
 let txt_of_cic_term size metasenv context t = 
   let fake_sequent = (-1,context,t) in
   txt_of_cic_sequent_conclusion size metasenv fake_sequent 
+;;
+
+ignore (
+ CicMetaSubst.set_ppterm_in_context
+  (fun ~metasenv subst term context ->
+    try
+     let context' = CicMetaSubst.apply_subst_context subst context in
+     let term' = CicMetaSubst.apply_subst subst term in
+      txt_of_cic_term 30 metasenv context' term'
+    with
+       Sys.Break as exn -> raise exn
+     | exn ->
+        "[[ Exception raised during pretty-printing: " ^
+        Printexc.to_string exn ^ " ]] " ^
+        CicMetaSubst.ppterm_in_context ~metasenv subst term context)
+);;
 
 (****************************************************************************)
 (* txt_of_cic_object: IMPROVE ME *)
diff --git a/matita/matita.ml b/matita/matita.ml
index 5717b710a..dc0aa579d 100644
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -214,6 +214,10 @@ let _ =
     );
     addDebugSeparator ();
 *)
+    addDebugItem "disable high level pretty printer"
+      (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := true);
+    addDebugItem "enable high level pretty printer"
+      (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := false);
     addDebugItem "disable all (pretty printing) notations"
       (fun _ -> CicNotation.set_active_notations []);
     addDebugItem "enable all (pretty printing) notations"
-- 
2.39.2