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.

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index c097eacf281869b9ff532d8e127ec80ac5d75d82..a86bc471a06f3a2f3a97b3b0082c965dd0ce8d12 100644 (file)
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/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/helm/software/components/cic_unification/cicMetaSubst.mli b/helm/software/components/cic_unification/cicMetaSubst.mli
index 2b60b04e02bb539672eb9b62f2d9fe1fe4ef386d..bc5b4c0390b480dc20ee3379713510e9e4a3124b 100644 (file)
--- a/helm/software/components/cic_unification/cicMetaSubst.mli
+++ b/helm/software/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/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 0678887cea809a6e4d75692df5c6ceaf2f98a388..920d1fef4bf634075470b586b2db59359cc30549 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/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/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 5717b710aa9925f48312e160b1c589884d22c13a..dc0aa579db5975ccbd4fab189c1f6de071b27929 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/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"