Acic2Procedural:

[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 2531620096f3a2ce1a65dae35a1c13faacbcf4a4..c9a3232484b30b60378dfc0da9b49bdd18996466 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -447,13 +447,15 @@ let get_flavour ?flavour attrs =
       | Some fl -> fl
       | None    -> aux attrs
 
-let proc_obj ?flavour st = function
+let proc_obj ?flavour ?(info="") st = function
    | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
       begin match get_flavour ?flavour attrs with
          | flavour when List.mem flavour th_flavours  ->
             let ast = proc_proof st v in
             let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
-            let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in
+            let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n"
+              "COMMENTS" info "tactics" steps "nodes" nodes
+           in
             T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
          | flavour when List.mem flavour def_flavours ->
             [T.Statement (flavour, Some s, t, Some v, "")]
@@ -469,8 +471,8 @@ let proc_obj ?flavour st = function
 
 (* interface functions ******************************************************)
 
-let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-   ?flavour prefix anobj = 
+let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types 
+   ?info ?depth ?flavour prefix anobj = 
    let st = {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
@@ -481,7 +483,7 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
    } in
    L.time_stamp "P : LEVEL 2  ";
    HLog.debug "Procedural: level 2 transformation";
-   let steps = proc_obj st ?flavour anobj in
+   let steps = proc_obj st ?flavour ?info anobj in
    L.time_stamp "P : RENDERING";
    HLog.debug "Procedural: grafite rendering";
    let r = List.rev (T.render_steps [] steps) in