ProceduralTeX completed and tested on the terms given as examples in the paper about...

[helm.git] / helm / software / components / acic_procedural / acic2Procedural.ml

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index ae64d1f19af4c904e804cd3dd3fd48001c525d9b..0edb5c8b041c9e2c5415790bd3a1badfca2ead20 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -45,6 +45,7 @@ module Cl   = ProceduralClassify
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
 module H    = ProceduralHelpers
+module X    = ProceduralTeX
 
 type status = {
    sorts : (C.id, A.sort_kind) Hashtbl.t;
@@ -55,6 +56,8 @@ type status = {
    case: int list
 }
 
+let tex_formatter = ref None
+
 let debug = ref false
 
 (* helpers ******************************************************************)
@@ -515,9 +518,13 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
       context     = [];
       case        = []
    } in
-   L.time_stamp "P : LEVEL 2  ";
-   HLog.debug "Procedural: level 2 transformation";
+   L.time_stamp "P : LEVEL 1  ";
+   HLog.debug "Procedural: level 1 transformation";
    let steps = proc_obj st ?flavour ?info anobj in
+   let _ = match !tex_formatter with
+      | None     -> ()
+      | Some frm -> X.tex_of_steps frm st.sorts steps
+   in
    L.time_stamp "P : RENDERING";
    HLog.debug "Procedural: grafite rendering";
    let r = List.rev (T.render_steps [] steps) in
@@ -533,7 +540,11 @@ let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
       context     = context;
       case        = []
    } in
-   HLog.debug "Procedural: level 2 transformation";
+   HLog.debug "Procedural: level 1 transformation";
    let steps = proc_proof st annterm in
+   let _ = match !tex_formatter with
+      | None     -> ()
+      | Some frm -> X.tex_of_steps frm st.sorts steps
+   in
    HLog.debug "Procedural: grafite rendering";
    List.rev (T.render_steps [] steps)