- Procedural: more support for the Debug inline option (does not work yet)

[helm.git] / helm / software / matita / applyTransformation.ml

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 4015293a435907f7a24f29f20b5824fb14e05cc1..f5f279e73dd55d6c819083562cfc6d16c39bdc64 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -46,6 +46,7 @@ module LS = LibrarySync
 module Ds = CicDischarge
 module PO = ProceduralOptimizer
 module N = CicNotationPt
+module A2P = Acic2Procedural
 
 let mpres_document pres_box =
   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
@@ -213,10 +214,12 @@ let txt_of_cic_object
              failwith msg
   in
   if List.mem G.IPProcedural params then begin
-(*
-     PO.debug := true;     
+
+     Procedural2.debug := A2P.is_debug 1 params;
+     PO.debug := A2P.is_debug 2 params;
+(*     
      PO.critical := false;
-     Acic2Procedural.tex_formatter := Some Format.std_formatter;       
+     A2P.tex_formatter := Some Format.std_formatter;   
      let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
 *)     
      let obj, info = PO.optimize_obj obj in
@@ -259,7 +262,7 @@ let txt_of_cic_object
            str
      in
      let script = 
-        Acic2Procedural.procedural_of_acic_object 
+        A2P.procedural_of_acic_object 
            ~ids_to_inner_sorts ~ids_to_inner_types ~info params aobj 
      in
      String.concat "" (List.map aux script) ^ "\n\n"
@@ -387,7 +390,7 @@ let procedural_txt_of_cic_term ~map_unicode_to_tex n params context term =
   let aux = GrafiteAstPp.pp_statement
      ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
   let script = 
-     Acic2Procedural.procedural_of_acic_term 
+     A2P.procedural_of_acic_term 
         ~ids_to_inner_sorts ~ids_to_inner_types params context annterm 
   in
   String.concat "" (List.map aux script)